mathlib
7e5137f5 - chore(*): add mathlib4 synchronization comments (#19165)

Commit
2 years ago
chore(*): add mathlib4 synchronization comments (#19165) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). 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`
Parents
Loading