Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-02 05:41 2ebc1d6c

View on Github →

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

  • algebraic_geometry.stalks
  • algebraic_geometry.structure_sheaf
  • analysis.analytic.basic
  • analysis.calculus.cont_diff_def
  • analysis.calculus.iterated_deriv
  • analysis.calculus.mean_value
  • analysis.inner_product_space.adjoint
  • analysis.inner_product_space.positive
  • analysis.normed_space.lp_equiv
  • analysis.normed_space.lp_space
  • measure_theory.constructions.pi
  • measure_theory.function.convergence_in_measure
  • measure_theory.function.locally_integrable
  • measure_theory.measure.haar.of_basis
  • probability.probability_mass_function.uniform
  • ring_theory.filtration
  • topology.algebra.valued_field
  • topology.metric_space.kuratowski

Estimated changes