Commit 2026-02-15 14:33 1d77eae4

View on Github →

chore: remove declarations deprecated between 2021-02-15 and 2025-08-15 (#35335) I am happy to remove some deprecated declarations for you! Please check if there are any remaining stray comments or other issues before merging.

Estimated changes

Modified Mathlib/Algebra/Algebra/Defs.lean

deleted theorem Algebra.id.map_eq_id

deleted theorem Algebra.id.map_eq_self

Modified Mathlib/Algebra/Colimit/Module.lean

deleted theorem AddCommGroup.DirectLimit.lift_unique

deleted theorem Module.DirectLimit.lift_unique

Modified Mathlib/Algebra/Colimit/Ring.lean

deleted theorem Ring.DirectLimit.lift_unique

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

deleted def MonoidHom.postcompEquiv

deleted def MonoidHom.precompEquiv

deleted def MulEquiv.monoidHomCongr

Modified Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean

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

Modified Mathlib/Algebra/Group/Support.lean

Modified Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

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

Modified Mathlib/Algebra/Module/ZLattice/Covolume.lean

Modified Mathlib/Algebra/Notation/Support.lean

Modified Mathlib/Algebra/Order/Group/Abs.lean

Modified Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean

Modified Mathlib/Algebra/Polynomial/Degree/Lemmas.lean

Modified Mathlib/Algebra/Polynomial/Monic.lean

Modified Mathlib/Algebra/Regular/SMul.lean

Modified Mathlib/Algebra/Ring/NonZeroDivisors.lean

Modified Mathlib/Algebra/Ring/Subsemiring/Defs.lean

Modified Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean

Modified Mathlib/Analysis/Calculus/Deriv/Pow.lean

deleted theorem deriv_fun_pow''

deleted theorem deriv_pow''

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

deleted theorem HasFDerivAtFilter.isBigO_sub_rev

deleted theorem HasStrictFDerivAt.isBigO_sub_rev

Modified Mathlib/Analysis/Convex/Hull.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean

deleted theorem Submodule.eq_starProjection_of_eq_submodule

Modified Mathlib/Analysis/InnerProductSpace/Projection/Submodule.lean

Modified Mathlib/Analysis/LocallyConvex/Polar.lean

Modified Mathlib/Analysis/Matrix/Order.lean

Modified Mathlib/Analysis/Matrix/Spectrum.lean

Modified Mathlib/Analysis/Meromorphic/NormalForm.lean

Modified Mathlib/Analysis/Normed/Module/WeakDual.lean

Modified Mathlib/Analysis/Normed/Ring/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

Modified Mathlib/CategoryTheory/Enriched/Basic.lean

Modified Mathlib/CategoryTheory/Functor/EpiMono.lean

Modified Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean

Modified Mathlib/CategoryTheory/Sites/Localization.lean

Modified Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean

Modified Mathlib/CategoryTheory/Triangulated/Subcategory.lean

Modified Mathlib/CategoryTheory/Yoneda.lean

Modified Mathlib/Data/EReal/Operations.lean

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/Data/Finset/Dedup.lean

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.head_cons_tail

Modified Mathlib/Data/List/Chain.lean

Modified Mathlib/Data/Matrix/Basis.lean

Modified Mathlib/Data/Matrix/Mul.lean

deleted theorem Matrix.mulVec_smul_assoc

Modified Mathlib/Data/Nat/Digits/Defs.lean

Modified Mathlib/Data/Nat/Factorization/PrimePow.lean

deleted theorem IsPrimePow.factorization_minFac_ne_zero

Modified Mathlib/Data/Nat/Init.lean

Modified Mathlib/Data/Rat/Cast/CharZero.lean

Modified Mathlib/Data/Set/Image.lean

deleted theorem Set.image_subset

Modified Mathlib/Data/TypeVec.lean

Modified Mathlib/Data/ZMod/Basic.lean

deleted theorem ZMod.eq_iff_modEq_nat

Modified Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean

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

Modified Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean

Modified Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean

Modified Mathlib/Geometry/Manifold/IntegralCurve/UniformTime.lean

Modified Mathlib/GroupTheory/Abelianization/Defs.lean

Modified Mathlib/GroupTheory/FreeAbelianGroup.lean

deleted theorem FreeAbelianGroup.lift.map_hom

Modified Mathlib/GroupTheory/GroupAction/Blocks.lean

Modified Mathlib/GroupTheory/GroupAction/SubMulAction/Pointwise.lean

Modified Mathlib/GroupTheory/Index.lean

Modified Mathlib/GroupTheory/MonoidLocalization/Basic.lean

Modified Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean

Modified Mathlib/LinearAlgebra/FreeModule/Basic.lean

Modified Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

Modified Mathlib/LinearAlgebra/Matrix/Hermitian.lean

Modified Mathlib/LinearAlgebra/Matrix/Ideal.lean

Modified Mathlib/LinearAlgebra/Projection.lean

Modified Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

deleted theorem MeasureTheory.SimpleFunc.eapprox_mono

Modified Mathlib/MeasureTheory/Group/MeasurableEquiv.lean

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

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

deleted theorem CompactlySupportedContinuousMap.monotone_of_nonneg

Modified Mathlib/MeasureTheory/Measure/DiracProba.lean

Modified Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean

Modified Mathlib/NumberTheory/DirichletCharacter/Basic.lean

Modified Mathlib/NumberTheory/ModularForms/SlashInvariantForms.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean

Modified Mathlib/NumberTheory/Padics/PadicIntegers.lean

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean

Modified Mathlib/NumberTheory/SelbergSieve.lean

Modified Mathlib/Order/Basic.lean

Modified Mathlib/Order/Monotone/Basic.lean

Modified Mathlib/Order/OrderIsoNat.lean

Modified Mathlib/Order/WellFounded.lean

Modified Mathlib/Probability/Independence/Integration.lean

Modified Mathlib/Probability/Kernel/Invariance.lean

deleted theorem ProbabilityTheory.Kernel.comp_const_apply_eq_bind

deleted theorem ProbabilityTheory.Kernel.const_bind_eq_comp_const

Modified Mathlib/Probability/Moments/CovarianceBilinDual.lean

Modified Mathlib/Probability/Moments/Variance.lean

Modified Mathlib/RepresentationTheory/Homological/GroupCohomology/Functoriality.lean

Modified Mathlib/RingTheory/AdjoinRoot.lean

Modified Mathlib/RingTheory/FiniteType.lean

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

Modified Mathlib/RingTheory/Ideal/AssociatedPrime/Localization.lean

Modified Mathlib/RingTheory/Ideal/IsPrimary.lean

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

deleted theorem AdjoinRoot.isAdjoinRootMonic_map_eq_mk

deleted theorem AdjoinRoot.isAdjoinRootMonic_root_eq_root

Modified Mathlib/RingTheory/Localization/AtPrime/Basic.lean

Modified Mathlib/RingTheory/Localization/Defs.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

deleted theorem MvPolynomial.noZeroDivisors_fin

deleted theorem MvPolynomial.noZeroDivisors_of_finite

Modified Mathlib/RingTheory/Regular/IsSMulRegular.lean

Modified Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean

deleted theorem ValuativeRel.vle_mul_left

Modified Mathlib/Topology/Algebra/ContinuousAffineEquiv.lean

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

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

Modified Mathlib/Topology/Algebra/Support.lean

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

Modified Mathlib/Topology/Compactification/StoneCech.lean

Modified Mathlib/Topology/ContinuousMap/CompactlySupported.lean

deleted theorem CompactlySupportedContinuousMap.toRealLinear_nonneg

Modified Mathlib/Topology/Instances/AddCircle/Defs.lean

deleted theorem AddCircle.addOrderOf_coe_eq_zero_iff_forall_rat_ne_div

Modified Mathlib/Topology/MetricSpace/Isometry.lean

Modified Mathlib/Topology/UnitInterval.lean

Modified docs/overview.yaml