Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-08 12:34 1a51edf1

View on Github →

chore(*): add mathlib4 synchronization comments (#19229) Regenerated from the port status wiki page. 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

Estimated changes