Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-02 06:16 f16e7a22

View on Github →

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

  • algebra.big_operators.fin
  • data.finset.finsupp
  • data.finset.functor
  • data.finset.pointwise
  • data.finsupp.basic
  • data.finsupp.big_operators
  • data.finsupp.pwo
  • data.multiset.locally_finite
  • data.set.pointwise.interval
  • group_theory.subgroup.pointwise
  • group_theory.submonoid.pointwise
  • order.compactly_generated
  • order.minimal
  • order.upper_lower.basic
  • order.well_founded_set
  • ring_theory.subsemiring.pointwise
  • topology.bases
  • topology.subset_properties

Estimated changes