Commit 2023-06-03 13:39 af471b9e
View on Github →chore(*): add mathlib4 synchronization comments (#19148) 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