Commit 2023-06-08 04:42 7e5137f5

chore(*): add mathlib4 synchronization comments (#19165) Regenerated from the port status wiki page. Relates to the following files:

• algebra.lie.classical
• analysis.calculus.bump_function_inner
• analysis.calculus.monotone
• analysis.calculus.parametric_interval_integral
• analysis.normed_space.quaternion_exponential
• analysis.special_functions.trigonometric.arctan_deriv
• analysis.special_functions.trigonometric.bounds
• category_theory.bicategory.coherence_tactic
• category_theory.monoidal.Mon_
• category_theory.monoidal.coherence
• category_theory.monoidal.subcategory
• category_theory.sites.compatible_plus
• category_theory.sites.types
• data.json
• data.real.pi.leibniz
• geometry.euclidean.angle.unoriented.right_angle
• linear_algebra.tensor_algebra.basic
• measure_theory.covering.density_theorem
• measure_theory.covering.differentiation
• measure_theory.covering.liminf_limsup
• measure_theory.covering.one_dim
• measure_theory.decomposition.lebesgue
• measure_theory.decomposition.radon_nikodym
• measure_theory.function.continuous_map_dense
• measure_theory.function.l2_space
• measure_theory.function.special_functions.arctan
• measure_theory.integral.interval_average
• measure_theory.integral.interval_integral
• measure_theory.integral.peak_function
• measure_theory.measure.finite_measure
• measure_theory.measure.haar.quotient
• measure_theory.measure.probability_measure
• probability.integration
• ring_theory.class_group
• ring_theory.roots_of_unity.basic
• ring_theory.roots_of_unity.complex
• topology.order.hom.esakia