Commit 2023-06-03 13:39 af471b9e

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