mathlib
1a51edf1 - chore(*): add mathlib4 synchronization comments (#19229)

Commit
2 years ago
chore(*): add mathlib4 synchronization comments (#19229) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.category.Algebra.basic` * `algebra.category.Algebra.limits` * `algebra.category.Module.change_of_rings` * `algebra.module.pid` * `algebraic_geometry.elliptic_curve.point` * `algebraic_geometry.morphisms.quasi_compact` * `algebraic_geometry.morphisms.quasi_separated` * `algebraic_geometry.projective_spectrum.structure_sheaf` * `algebraic_topology.fundamental_groupoid.induced_maps` * `algebraic_topology.fundamental_groupoid.product` * `algebraic_topology.fundamental_groupoid.simply_connected` * `analysis.normed.group.SemiNormedGroup.kernels` * `category_theory.adjunction.lifting` * `category_theory.monoidal.internal.Module` * `data.qpf.multivariate.constructions.cofix` * `geometry.manifold.diffeomorph` * `geometry.manifold.vector_bundle.smooth_section` * `geometry.manifold.whitney_embedding` * `group_theory.finite_abelian` * `linear_algebra.clifford_algebra.contraction` * `linear_algebra.exterior_algebra.grading` * `linear_algebra.matrix.schur_complement` * `linear_algebra.tensor_algebra.to_tensor_power` * `model_theory.direct_limit` * `model_theory.fraisse` * `number_theory.modular_forms.basic` * `representation_theory.character` * `representation_theory.group_cohomology.basic` * `ring_theory.jacobson` * `ring_theory.nullstellensatz` * `topology.metric_space.gromov_hausdorff` * `topology.vector_bundle.hom`
Parents
Loading