Commit 2023-06-06 05:16 36938f77

chore(*): add mathlib4 synchronization comments (#19159) 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