Commit 2025-12-17 19:48 d24b8b34

View on Github →

chore: remove March and April 2025 deprecated declarations (#32990) I undeprecate Nat.Ico_succ_right_eq_insert_Ico, since it is a natural counterpart to the nondeprecated Nat.Ico_succ_left_eq_erase_Ico.

Estimated changes

Modified Mathlib/Algebra/Algebra/Basic.lean

Modified Mathlib/Algebra/GroupWithZero/Commute.lean

Modified Mathlib/Algebra/GroupWithZero/Units/Basic.lean

Modified Mathlib/Algebra/Module/Equiv/Basic.lean

Modified Mathlib/Algebra/Module/LinearMap/End.lean

Modified Mathlib/Algebra/Ring/Basic.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Operations.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Mul.lean

Modified Mathlib/Analysis/Calculus/TangentCone/Basic.lean

Modified Mathlib/Analysis/Calculus/TangentCone/Defs.lean

Modified Mathlib/Analysis/Calculus/TangentCone/DimOne.lean

Modified Mathlib/Analysis/Calculus/TangentCone/Pi.lean

Modified Mathlib/Analysis/Calculus/TangentCone/Prod.lean

Modified Mathlib/Analysis/Calculus/TangentCone/ProperSpace.lean

Modified Mathlib/Analysis/Calculus/TangentCone/Real.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

Modified Mathlib/Analysis/InnerProductSpace/Defs.lean

Modified Mathlib/Analysis/Meromorphic/Order.lean

Modified Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean

deleted theorem CategoryTheory.preservesShape_fin_of_preserves_binary_and_terminal

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean

Modified Mathlib/CategoryTheory/Monoidal/Closed/Ideal.lean

Modified Mathlib/Combinatorics/Additive/CauchyDavenport.lean

Modified Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

Modified Mathlib/Combinatorics/SimpleGraph/Paths.lean

Modified Mathlib/Data/ENNReal/Operations.lean

Modified Mathlib/Data/Fin/Basic.lean

Modified Mathlib/Data/List/Sigma.lean

Modified Mathlib/Dynamics/PeriodicPts/Defs.lean

Modified Mathlib/Dynamics/PeriodicPts/Lemmas.lean

Modified Mathlib/Geometry/Manifold/IsManifold/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

Modified Mathlib/LinearAlgebra/Multilinear/Curry.lean

Modified Mathlib/LinearAlgebra/Projectivization/Independence.lean

Modified Mathlib/MeasureTheory/Function/L2Space.lean

Modified Mathlib/MeasureTheory/Group/Arithmetic.lean

Modified Mathlib/MeasureTheory/Integral/Average.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/Basic.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Markov.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Sub.lean

Modified Mathlib/Order/Filter/AtTopBot/Basic.lean

Modified Mathlib/Order/Interval/Finset/Nat.lean

deleted theorem Nat.Icc_insert_succ_left

deleted theorem Nat.Icc_insert_succ_right

deleted theorem Nat.Icc_pred_right

deleted theorem Nat.Icc_succ_left

deleted theorem Nat.Ico_insert_succ_left

deleted theorem Nat.Ico_succ_left

deleted theorem Nat.Ico_succ_right

modified theorem Nat.Ico_succ_right_eq_insert_Ico

deleted theorem Nat.Ico_succ_succ

Modified Mathlib/RepresentationTheory/Tannaka.lean

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

deleted theorem IsDedekindDomain.HeightOneSpectrum.intValuation_toFun

Modified Mathlib/RingTheory/Polynomial/Eisenstein/Distinguished.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/Topology/Algebra/Module/Equiv.lean

Modified Mathlib/Topology/Algebra/Order/Field.lean

Modified Mathlib/Topology/Algebra/Valued/ValuationTopology.lean

Modified Mathlib/Topology/UniformSpace/Defs.lean