Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-09 01:31 b6da1a0b

View on Github →

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

  • combinatorics.simple_graph.regularity.equitabilise
  • data.dfinsupp.interval
  • data.finsupp.interval
  • data.set.mul_antidiagonal
  • group_theory.divisible
  • linear_algebra.affine_space.basic
  • order.upper_lower.hom
  • ring_theory.ore_localization.basic
  • topology.algebra.order.liminf_limsup
  • topology.filter
  • topology.order.hom.basic

Estimated changes