Closed github-actions[bot] closed 1 year ago
bors r+
Pull request successfully merged into master.
Build succeeded!
The publicly hosted instance of bors-ng is deprecated and will go away soon.
If you want to self-host your own instance, instructions are here. For more help, visit the forum.
If you want to switch to GitHub's built-in merge queue, visit their help page.
Regenerated from the port status wiki page. Relates to the following files:
algebra.category.Module.monoidal.symmetric
algebra.lie.base_change
algebra.lie.character
algebra.lie.direct_sum
algebra.lie.semisimple
algebra.lie.skew_adjoint
algebra.lie.solvable
algebra.module.dedekind_domain
algebra.symmetrized
analysis.ODE.gronwall
analysis.box_integral.partition.measure
analysis.calculus.fderiv_analytic
analysis.calculus.series
analysis.inner_product_space.calculus
analysis.inner_product_space.euclidean_dist
analysis.special_functions.arsinh
analysis.special_functions.bernstein
analysis.special_functions.compare_exp
analysis.special_functions.complex.log_deriv
analysis.special_functions.log.deriv
analysis.special_functions.trigonometric.deriv
analysis.special_functions.trigonometric.inverse_deriv
category_theory.bicategory.natural_transformation
category_theory.monoidal.of_chosen_finite_products.symmetric
category_theory.monoidal.rigid.functor_category
category_theory.monoidal.rigid.of_equivalence
category_theory.monoidal.types.symmetric
category_theory.sites.canonical
data.complex.exponential_bounds
data.nat.sqrt_norm_num
field_theory.laurent
geometry.manifold.instances.real
geometry.manifold.instances.units_of_normed_algebra
geometry.manifold.metrizable
geometry.manifold.smooth_manifold_with_corners
group_theory.transfer
linear_algebra.quadratic_form.basic
measure_theory.integral.bochner
measure_theory.integral.vitali_caratheodory
measure_theory.measure.haar.normed_space
measure_theory.measure.lebesgue.eq_haar
number_theory.liouville.measure
ring_theory.dedekind_domain.ideal
ring_theory.polynomial.bernstein
ring_theory.witt_vector.defs
ring_theory.witt_vector.structure_polynomial
topology.continuous_function.stone_weierstrass
topology.continuous_function.weierstrass
The following files have no module docstring, so I have not added a message in this PR
control.basic
data.bitvec.basic
data.seq.computation
data.seq.parallel
data.seq.seq
data.seq.wseq
Please make a PR to add a module docstring (for Lean3 and Lean4!), then I will add the freeze comment next time.
The following files no longer exist in Lean 3' mathlib, so I have not added a message in this PR
lean_core.data.vector
In future we should find where they moved to, and check that the files are still in sync.
I am a bot; please check that I have not put a comment in a bad place before running
bors merge
!