mathlib3
af471b9e - chore(*): add mathlib4 synchronization comments (#19148)

Commit
2 years ago
chore(*): add mathlib4 synchronization comments (#19148) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.gcd_monoid.integrally_closed` * `algebra.lie.submodule` * `algebraic_geometry.locally_ringed_space` * `algebraic_geometry.ringed_space` * `analysis.analytic.linear` * `analysis.analytic.radius_liminf` * `analysis.calculus.extend_deriv` * `analysis.calculus.lhopital` * `analysis.calculus.taylor` * `analysis.calculus.uniform_limits_deriv` * `analysis.inner_product_space.l2_space` * `analysis.inner_product_space.orientation` * `analysis.normed_space.exponential` * `analysis.normed_space.star.exponential` * `analysis.von_neumann_algebra.basic` * `category_theory.extensive` * `category_theory.monoidal.braided` * `category_theory.monoidal.rigid.basic` * `data.mv_polynomial.derivation` * `data.ordmap.ordset` * `field_theory.finite.basic` * `field_theory.finite.polynomial` * `linear_algebra.matrix.charpoly.finite_field` * `measure_theory.function.simple_func_dense_lp` * `measure_theory.function.strongly_measurable.lp` * `measure_theory.function.uniform_integrable` * `measure_theory.integral.set_to_l1` * `measure_theory.measure.lebesgue.basic` * `measure_theory.measure.lebesgue.complex` * `number_theory.liouville.basic` * `number_theory.liouville.liouville_with` * `number_theory.liouville.residual` * `probability.independence.basic` * `probability.independence.zero_one` * `ring_theory.derivation.basic` * `ring_theory.integrally_closed` * `ring_theory.polynomial.rational_root` * `ring_theory.valuation.integral` * `topology.homotopy.H_spaces`
Parents
Loading