Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-08 07:36 3e32bc90

View on Github →

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

  • algebra.add_torsor
  • category_theory.bicategory.basic
  • data.finsupp.antidiagonal
  • data.nat.choose.central
  • data.nat.choose.sum
  • number_theory.primorial
  • order.liminf_limsup
  • topology.algebra.order.extend_from
  • topology.continuous_function.cocompact_map
  • topology.locally_constant.basic
  • topology.order.lattice
  • topology.sober
  • topology.stone_cech

Estimated changes