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.algebra.spectrum
algebra.category.Module.algebra
algebra.lie.free
algebra.lie.normalizer
algebra.lie.quotient
algebra.lie.universal_enveloping
algebra.order.complete_field
algebra.order.interval
algebra.star.order
analysis.normed_space.enorm
analysis.special_functions.integrals
analysis.special_functions.non_integrable
analysis.special_functions.polar_coord
category_theory.monoidal.of_has_finite_products
category_theory.monoidal.opposite
category_theory.monoidal.skeleton
category_theory.monoidal.types.coyoneda
category_theory.preadditive.Mat
data.rat.star
data.real.pi.wallis
field_theory.adjoin
group_theory.schur_zassenhaus
linear_algebra.eigenspace.basic
linear_algebra.tensor_algebra.grading
measure_theory.covering.besicovitch
measure_theory.covering.besicovitch_vector_space
measure_theory.function.jacobian
measure_theory.integral.divergence_theorem
measure_theory.integral.fund_thm_calculus
measure_theory.measure.lebesgue.integral
number_theory.ramification_inertia
ring_theory.dedekind_domain.dvr
ring_theory.dedekind_domain.pid
ring_theory.discrete_valuation_ring.tfae
ring_theory.polynomial.cyclotomic.basic
ring_theory.witt_vector.basic
ring_theory.witt_vector.is_poly
ring_theory.witt_vector.mul_p
ring_theory.witt_vector.teichmuller
topology.algebra.continuous_affine_map
topology.algebra.module.character_space
topology.category.Compactum
topology.continuous_function.units
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
!