Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-22 06:13 c085f304

View on Github →

chore(*): add mathlib4 synchronization comments (#18630) Regenerated from the port status wiki page. Relates to the following files:

  • algebra.category.Mon.basic
  • algebra.squarefree
  • category_theory.closed.monoidal
  • category_theory.single_obj
  • data.zmod.coprime
  • field_theory.perfect_closure
  • linear_algebra.invariant_basis_number
  • ring_theory.euclidean_domain
  • ring_theory.flat
  • ring_theory.int.basic
  • ring_theory.principal_ideal_domain
  • ring_theory.unique_factorization_domain

Estimated changes