Commit 2025-08-12 06:50 cff2a6ea

View on Github →

chore: remove >6 month old deprecations (#28212)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean

Modified Mathlib/Algebra/Group/Equiv/Defs.lean

Modified Mathlib/Algebra/Group/Subgroup/Ker.lean

Modified Mathlib/Algebra/Group/Submonoid/Operations.lean

Modified Mathlib/CategoryTheory/Sites/Subsheaf.lean

Modified Mathlib/CategoryTheory/Subpresheaf/Basic.lean

Modified Mathlib/CategoryTheory/Subpresheaf/Image.lean

Modified Mathlib/Combinatorics/Additive/RuzsaCovering.lean

Modified Mathlib/Computability/Encoding.lean

deleted theorem Computability.leftInverse_section_inclusion

Modified Mathlib/Computability/Primrec.lean

Modified Mathlib/Data/ENNReal/Basic.lean

deleted theorem ENNReal.two_lt_top

deleted theorem ENNReal.two_ne_top

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/List/Enum.lean

Modified Mathlib/Data/List/FinRange.lean

Modified Mathlib/Data/List/Indexes.lean

deleted theorem List.findIdxs_eq_map_indexesValues

deleted theorem List.foldlIdxM_eq_foldlM_enum

deleted def List.foldlIdxSpec

deleted theorem List.foldlIdxSpec_cons

deleted theorem List.foldlIdx_eq_foldlIdxSpec

deleted theorem List.foldlIdx_eq_foldl_enum

deleted theorem List.foldrIdxM_eq_foldrM_enum

deleted def List.foldrIdxSpec

deleted theorem List.foldrIdxSpec_cons

deleted theorem List.foldrIdx_eq_foldrIdxSpec

deleted theorem List.foldrIdx_eq_foldr_enum

deleted theorem List.get_mapIdx

deleted theorem List.indexesValues_eq_filter_enum

deleted theorem List.list_reverse_induction

deleted def List.mapIdxMAuxSpec

deleted theorem List.mapIdxMAuxSpec_cons

deleted theorem List.mapIdxMGo_eq_mapIdxMAuxSpec

deleted theorem List.mapIdxM_eq_mmap_enum

deleted theorem List.map_enumFrom_eq_zipWith

Modified Mathlib/Data/List/Nodup.lean

Modified Mathlib/Data/List/Sigma.lean

Modified Mathlib/Data/Matrix/Mul.lean

Modified Mathlib/Data/Matrix/PEquiv.lean

Modified Mathlib/Data/Matroid/Basic.lean

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/Data/Set/Card.lean

Modified Mathlib/Data/Set/Finite/Basic.lean

Modified Mathlib/Geometry/Manifold/Algebra/LieGroup.lean

Modified Mathlib/Geometry/Manifold/Algebra/Monoid.lean

Modified Mathlib/Geometry/Manifold/Algebra/Structures.lean

Modified Mathlib/Geometry/Manifold/DerivationBundle.lean

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

Modified Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean

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

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

Modified Mathlib/RingTheory/Multiplicity.lean