mathlib3
fd4551cf - chore(*): add mathlib4 synchronization comments (#19171)

Commit
2 years ago
chore(*): add mathlib4 synchronization comments (#19171) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.lie.cartan_subalgebra` * `algebra.lie.nilpotent` * `analysis.ODE.picard_lindelof` * `analysis.calculus.affine_map` * `analysis.complex.abs_max` * `analysis.complex.cauchy_integral` * `analysis.complex.liouville` * `analysis.complex.locally_uniform_limit` * `analysis.complex.phragmen_lindelof` * `analysis.complex.removable_singularity` * `analysis.complex.schwarz` * `analysis.convex.measure` * `analysis.fourier.fourier_transform` * `analysis.normed_space.add_torsor_bases` * `analysis.normed_space.continuous_affine_map` * `analysis.special_functions.improper_integrals` * `analysis.special_functions.stirling` * `analysis.special_functions.trigonometric.euler_sine_prod` * `analysis.sum_integral_comparisons` * `category_theory.closed.cartesian` * `category_theory.closed.types` * `category_theory.closed.zero` * `category_theory.monoidal.Mod_` * `data.real.pi.bounds` * `data.vector3` * `field_theory.fixed` * `field_theory.is_alg_closed.basic` * `field_theory.normal` * `measure_theory.group.geometry_of_numbers` * `measure_theory.group.integration` * `measure_theory.integral.circle_integral` * `measure_theory.integral.circle_transform` * `measure_theory.integral.exp_decay` * `measure_theory.integral.integral_eq_improper` * `measure_theory.integral.layercake` * `number_theory.bernoulli_polynomials` * `probability.kernel.basic` * `topology.category.Profinite.cofiltered_limit`
Parents
Loading