Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-19 06:10 1dac236e

View on Github →

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

  • algebra.group_ring_action.invariant
  • algebra.quadratic_discriminant
  • data.dfinsupp.well_founded
  • data.mv_polynomial.comm_ring
  • data.mv_polynomial.invertible
  • data.mv_polynomial.supported
  • data.mv_polynomial.variables
  • data.zmod.basic
  • ring_theory.finiteness
  • ring_theory.multiplicity
  • ring_theory.polynomial.chebyshev
  • ring_theory.valuation.integers
  • topology.category.Born

Estimated changes