Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-31 08:02 61b5e275

View on Github →

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

  • algebra.category.Module.adjunctions
  • analysis.calculus.darboux
  • analysis.calculus.deriv.inv
  • analysis.calculus.diff_cont_on_cl
  • analysis.calculus.dslope
  • analysis.inner_product_space.gram_schmidt_ortho
  • category_theory.abelian.ext
  • category_theory.abelian.left_derived
  • category_theory.bicategory.single_obj
  • data.real.golden_ratio
  • measure_theory.category.Meas
  • measure_theory.decomposition.jordan
  • measure_theory.decomposition.signed_hahn
  • measure_theory.group.action
  • measure_theory.group.measure
  • number_theory.arithmetic_function
  • number_theory.l_series
  • number_theory.von_mangoldt
  • topology.algebra.continuous_monoid_hom
  • topology.instances.discrete
  • topology.sheaves.stalks
  • topology.tietze_extension

Estimated changes