mathlib
6b31d1ee - chore(*): add mathlib4 synchronization comments (#19167)

Commit
2 years ago
chore(*): add mathlib4 synchronization comments (#19167) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.algebra.spectrum` * `algebra.category.Module.algebra` * `algebra.lie.free` * `algebra.lie.normalizer` * `algebra.lie.quotient` * `algebra.lie.universal_enveloping` * `algebra.order.complete_field` * `algebra.order.interval` * `algebra.star.order` * `analysis.normed_space.enorm` * `analysis.special_functions.integrals` * `analysis.special_functions.non_integrable` * `analysis.special_functions.polar_coord` * `category_theory.monoidal.of_has_finite_products` * `category_theory.monoidal.opposite` * `category_theory.monoidal.skeleton` * `category_theory.monoidal.types.coyoneda` * `category_theory.preadditive.Mat` * `data.rat.star` * `data.real.pi.wallis` * `field_theory.adjoin` * `group_theory.schur_zassenhaus` * `linear_algebra.eigenspace.basic` * `linear_algebra.tensor_algebra.grading` * `measure_theory.covering.besicovitch` * `measure_theory.covering.besicovitch_vector_space` * `measure_theory.function.jacobian` * `measure_theory.integral.divergence_theorem` * `measure_theory.integral.fund_thm_calculus` * `measure_theory.measure.lebesgue.integral` * `number_theory.ramification_inertia` * `ring_theory.dedekind_domain.dvr` * `ring_theory.dedekind_domain.pid` * `ring_theory.discrete_valuation_ring.tfae` * `ring_theory.polynomial.cyclotomic.basic` * `ring_theory.witt_vector.basic` * `ring_theory.witt_vector.is_poly` * `ring_theory.witt_vector.mul_p` * `ring_theory.witt_vector.teichmuller` * `topology.algebra.continuous_affine_map` * `topology.algebra.module.character_space` * `topology.category.Compactum` * `topology.continuous_function.units`
Parents
Loading