Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-30 08:50 f60c6087

View on Github →

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

  • algebra.category.Group.biproducts
  • algebra.category.Module.monoidal.basic
  • algebra.category.Ring.adjunctions
  • algebra.monoid_algebra.grading
  • analysis.calculus.deriv.add
  • analysis.calculus.deriv.basic
  • analysis.calculus.deriv.comp
  • analysis.calculus.deriv.inverse
  • analysis.calculus.deriv.linear
  • analysis.calculus.deriv.mul
  • analysis.calculus.deriv.polynomial
  • analysis.calculus.deriv.pow
  • analysis.calculus.deriv.prod
  • analysis.calculus.deriv.slope
  • analysis.calculus.deriv.star
  • analysis.calculus.deriv.support
  • analysis.calculus.fderiv_measurable
  • analysis.calculus.local_extr
  • analysis.convex.cone.dual
  • analysis.inner_product_space.lax_milgram
  • analysis.inner_product_space.pi_L2
  • category_theory.bicategory.coherence
  • category_theory.limits.fubini
  • category_theory.monoidal.coherence_lemmas
  • geometry.euclidean.sphere.basic
  • geometry.euclidean.sphere.power
  • geometry.euclidean.sphere.second_inter
  • group_theory.complement
  • group_theory.sylow
  • linear_algebra.matrix.hermitian
  • measure_theory.constructions.prod.basic
  • measure_theory.function.lp_order
  • measure_theory.function.lp_seminorm
  • measure_theory.function.lp_space
  • measure_theory.measure.complex
  • measure_theory.measure.vector_measure
  • number_theory.padics.ring_homs
  • ring_theory.ideal.cotangent
  • topology.metric_space.metrizable_uniformity
  • topology.sheaves.forget
  • topology.sheaves.sheaf_condition.unique_gluing
  • topology.sheaves.sheaf_of_functions

Estimated changes