mathlib
c2092722 - chore(*): add mathlib4 synchronization comments (#19162)

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