[Merged by Bors] - chore(*): add mathlib4 synchronization comments #19148
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Regenerated from the port status wiki page.
Relates to the following files:
algebra.gcd_monoid.integrally_closed
algebra.lie.submodule
algebraic_geometry.locally_ringed_space
algebraic_geometry.ringed_space
analysis.analytic.linear
analysis.analytic.radius_liminf
analysis.calculus.extend_deriv
analysis.calculus.lhopital
analysis.calculus.taylor
analysis.calculus.uniform_limits_deriv
analysis.inner_product_space.l2_space
analysis.inner_product_space.orientation
analysis.normed_space.exponential
analysis.normed_space.star.exponential
analysis.von_neumann_algebra.basic
category_theory.extensive
category_theory.monoidal.braided
category_theory.monoidal.rigid.basic
data.mv_polynomial.derivation
data.ordmap.ordset
field_theory.finite.basic
field_theory.finite.polynomial
linear_algebra.matrix.charpoly.finite_field
measure_theory.function.simple_func_dense_lp
measure_theory.function.strongly_measurable.lp
measure_theory.function.uniform_integrable
measure_theory.integral.set_to_l1
measure_theory.measure.lebesgue.basic
measure_theory.measure.lebesgue.complex
number_theory.liouville.basic
number_theory.liouville.liouville_with
number_theory.liouville.residual
probability.independence.basic
probability.independence.zero_one
ring_theory.derivation.basic
ring_theory.integrally_closed
ring_theory.polynomial.rational_root
ring_theory.valuation.integral
topology.homotopy.H_spaces
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
!