mathlib
a87d2257 - chore(*): add mathlib4 synchronization comments (#19089)

Commit
2 years ago
chore(*): add mathlib4 synchronization comments (#19089) 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.filtered_colimits` * `algebra.category.Module.limits` * `algebra.direct_limit` * `algebraic_geometry.prime_spectrum.basic` * `algebraic_geometry.prime_spectrum.is_open_comap_C` * `analysis.calculus.fderiv.star` * `analysis.complex.isometry` * `analysis.locally_convex.with_seminorms` * `analysis.normed.mul_action` * `analysis.normed_space.hahn_banach.extension` * `data.fintype.quotient` * `field_theory.separable_degree` * `linear_algebra.charpoly.to_matrix` * `linear_algebra.matrix.general_linear_group` * `linear_algebra.matrix.to_linear_equiv` * `measure_theory.function.ae_eq_fun` * `model_theory.quotients` * `number_theory.modular_forms.congruence_subgroups` * `ring_theory.adjoin.power_basis` * `ring_theory.adjoin_root` * `ring_theory.laurent_series` * `topology.instances.rat_lemmas` * `topology.metric_space.gromov_hausdorff_realized`
Parents
Loading