mathlib3
4280f5f3 - chore(*): add mathlib4 synchronization comments (#19057)

Commit
2 years ago
chore(*): add mathlib4 synchronization comments (#19057) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.category.Group.limits` * `algebra.category.Module.kernels` * `algebra.category.Mon.filtered_colimits` * `algebra.char_p.mixed_char_zero` * `algebraic_geometry.presheafed_space` * `algebraic_geometry.projective_spectrum.topology` * `analysis.calculus.fderiv.basic` * `analysis.normed_space.star.mul` * `analysis.special_functions.complex.circle` * `analysis.special_functions.pow.nnreal` * `linear_algebra.matrix.charpoly.basic` * `linear_algebra.matrix.charpoly.coeff` * `linear_algebra.matrix.charpoly.linear_map` * `measure_theory.constructions.borel_space.basic` * `measure_theory.constructions.borel_space.complex` * `measure_theory.constructions.borel_space.continuous_linear_map` * `measure_theory.constructions.polish` * `measure_theory.function.ae_measurable_order` * `measure_theory.function.ess_sup` * `measure_theory.function.floor` * `measure_theory.function.simple_func` * `measure_theory.function.simple_func_dense` * `measure_theory.function.special_functions.basic` * `measure_theory.integral.lebesgue` * `measure_theory.measure.regular` * `measure_theory.measure.stieltjes` * `number_theory.class_number.admissible_card_pow_degree` * `ring_theory.graded_algebra.homogeneous_ideal` * `ring_theory.graded_algebra.homogeneous_localization` * `ring_theory.ideal.minimal_prime` * `ring_theory.polynomial_algebra` * `topology.algebra.module.locally_convex` * `topology.continuous_function.bounded` * `topology.sheaves.sheaf_condition.sites`
Parents
Loading