mathlib3
36938f77 - chore(*): add mathlib4 synchronization comments (#19159)

Commit
2 years ago
chore(*): add mathlib4 synchronization comments (#19159) 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.monoidal.symmetric` * `algebra.lie.base_change` * `algebra.lie.character` * `algebra.lie.direct_sum` * `algebra.lie.semisimple` * `algebra.lie.skew_adjoint` * `algebra.lie.solvable` * `algebra.module.dedekind_domain` * `algebra.symmetrized` * `analysis.ODE.gronwall` * `analysis.box_integral.partition.measure` * `analysis.calculus.fderiv_analytic` * `analysis.calculus.series` * `analysis.inner_product_space.calculus` * `analysis.inner_product_space.euclidean_dist` * `analysis.special_functions.arsinh` * `analysis.special_functions.bernstein` * `analysis.special_functions.compare_exp` * `analysis.special_functions.complex.log_deriv` * `analysis.special_functions.log.deriv` * `analysis.special_functions.trigonometric.deriv` * `analysis.special_functions.trigonometric.inverse_deriv` * `category_theory.bicategory.natural_transformation` * `category_theory.monoidal.of_chosen_finite_products.symmetric` * `category_theory.monoidal.rigid.functor_category` * `category_theory.monoidal.rigid.of_equivalence` * `category_theory.monoidal.types.symmetric` * `category_theory.sites.canonical` * `data.complex.exponential_bounds` * `data.nat.sqrt_norm_num` * `field_theory.laurent` * `geometry.manifold.instances.real` * `geometry.manifold.instances.units_of_normed_algebra` * `geometry.manifold.metrizable` * `geometry.manifold.smooth_manifold_with_corners` * `group_theory.transfer` * `linear_algebra.quadratic_form.basic` * `measure_theory.integral.bochner` * `measure_theory.integral.vitali_caratheodory` * `measure_theory.measure.haar.normed_space` * `measure_theory.measure.lebesgue.eq_haar` * `number_theory.liouville.measure` * `ring_theory.dedekind_domain.ideal` * `ring_theory.polynomial.bernstein` * `ring_theory.witt_vector.defs` * `ring_theory.witt_vector.structure_polynomial` * `topology.continuous_function.stone_weierstrass` * `topology.continuous_function.weierstrass`
Parents
Loading