Commit 2023-06-07 05:24 c2092722

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

• algebra.category.Module.colimits
• algebra.category.Module.monoidal.closed
• algebra.homology.local_cohomology
• analysis.box_integral.basic
• analysis.box_integral.divergence_theorem
• analysis.box_integral.integrability
• analysis.calculus.parametric_integral
• analysis.convex.integral
• analysis.convex.specific_functions.deriv
• analysis.special_functions.exponential
• analysis.special_functions.pow.deriv
• analysis.special_functions.trigonometric.arctan
• analysis.special_functions.trigonometric.complex
• analysis.special_functions.trigonometric.complex_deriv
• analysis.special_functions.trigonometric.series
• category_theory.closed.functor_category
• category_theory.with_terminal
• combinatorics.additive.behrend
• combinatorics.derangements.exponential
• data.set.ncard
• field_theory.splitting_field.is_splitting_field
• group_theory.schreier
• group_theory.specific_groups.quaternion
• linear_algebra.quadratic_form.complex
• linear_algebra.quadratic_form.isometry
• linear_algebra.quadratic_form.prod
• linear_algebra.quadratic_form.real
• measure_theory.constructions.prod.integral
• measure_theory.function.ae_eq_of_integral
• measure_theory.group.fundamental_domain
• measure_theory.integral.average
• measure_theory.integral.set_integral
• measure_theory.measure.haar.inner_product_space
• measure_theory.measure.with_density_vector_measure
• representation_theory.Action
• ring_theory.dedekind_domain.factorization
• ring_theory.localization.away.adjoin_root
• ring_theory.valuation.valuation_ring