Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-01 06:32 599fffe7

View on Github →

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

  • analysis.calculus.deriv.zpow
  • analysis.quaternion
  • analysis.specific_limits.floor_pow
  • category_theory.sites.closed
  • group_theory.nilpotent
  • measure_theory.function.l1_space
  • measure_theory.group.prod
  • measure_theory.integral.integrable_on
  • measure_theory.measure.haar.basic
  • topology.homotopy.homotopy_group
  • topology.sheaves.local_predicate

Estimated changes