Commit 2026-05-17 20:27 b2958bc1

View on Github →

chore: remove declarations deprecated between 2021-05-15 and 2025-11-15 (#39405) 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/Basic.lean

deleted theorem algebraMap.lift_map_eq_zero_iff

Modified Mathlib/Algebra/BigOperators/Finsupp/Basic.lean

deleted theorem Finsupp.sum_sum_index'

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

Modified Mathlib/Algebra/Category/ModuleCat/Sheaf/Generators.lean

Modified Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean

Modified Mathlib/Algebra/CharP/Frobenius.lean

deleted theorem frobenius_add

deleted theorem frobenius_mul

deleted theorem frobenius_natCast

deleted theorem frobenius_neg

deleted theorem frobenius_one

deleted theorem frobenius_sub

deleted theorem frobenius_zero

Modified Mathlib/Algebra/CubicDiscriminant.lean

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

deleted def Add.toVAdd

deleted def Mul.toSMul

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

Modified Mathlib/Algebra/Group/Torsion.lean

Modified Mathlib/Algebra/Group/TypeTags/Hom.lean

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

Modified Mathlib/Algebra/Homology/ShortComplex/Ab.lean

Modified Mathlib/Algebra/Module/Submodule/Ker.lean

deleted theorem LinearMap.disjoint_ker'

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

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

Modified Mathlib/Algebra/Order/Ring/Cast.lean

Modified Mathlib/Algebra/Order/Ring/Pow.lean

deleted theorem one_add_mul_le_pow'

Modified Mathlib/Algebra/Order/Star/Basic.lean

Modified Mathlib/Algebra/Polynomial/Basic.lean

deleted theorem Polynomial.monomial_add

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

Modified Mathlib/Algebra/Polynomial/Monic.lean

Modified Mathlib/Algebra/Ring/Equiv.lean

Modified Mathlib/Algebra/Ring/GeomSum.lean

Modified Mathlib/Algebra/Ring/Parity.lean

Modified Mathlib/Algebra/Ring/Subring/Basic.lean

deleted theorem Subring.toAddSubgroup_le_toAddSubgroup

deleted theorem Subring.toAddSubgroup_lt_toAddSubgroup

deleted theorem Subring.toSubsemiring_le_toSubsemiring

deleted theorem Subring.toSubsemiring_lt_toSubsemiring

Modified Mathlib/Algebra/Star/Unitary.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean

deleted theorem SSet.OneTruncation₂.HoRel₂.mk

deleted theorem SSet.OneTruncation₂.id_edge

Modified Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

Modified Mathlib/Analysis/CStarAlgebra/Spectrum.lean

Modified Mathlib/Analysis/CStarAlgebra/Unitary/Connected.lean

Modified Mathlib/Analysis/Complex/Exponential.lean

deleted theorem Real.exp_lt_exp_of_lt

Modified Mathlib/Analysis/Complex/Norm.lean

Modified Mathlib/Analysis/Convex/Slope.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace/Fourier.lean

Modified Mathlib/Analysis/Distribution/TemperateGrowth.lean

Modified Mathlib/Analysis/Fourier/FourierTransform.lean

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

Modified Mathlib/Analysis/InnerProductSpace/Dual.lean

Modified Mathlib/Analysis/InnerProductSpace/LinearMap.lean

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

Modified Mathlib/Analysis/LocallyConvex/Bounded.lean

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

Modified Mathlib/Analysis/Matrix/Order.lean

Modified Mathlib/Analysis/Matrix/PosDef.lean

Modified Mathlib/Analysis/Matrix/Spectrum.lean

Modified Mathlib/Analysis/Normed/Algebra/Exponential.lean

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

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

Modified Mathlib/Analysis/Normed/Operator/Bilinear.lean

deleted theorem ContinuousLinearMap.norm_smulRightL_apply

Modified Mathlib/Analysis/SpecialFunctions/Log/ERealExp.lean

deleted theorem EReal.exp_le_exp

deleted theorem EReal.exp_lt_exp

Modified Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

deleted theorem Mathlib.Meta.NormNum.isInt_rpow_neg

deleted theorem Mathlib.Meta.NormNum.isInt_rpow_pos

deleted theorem Mathlib.Meta.NormNum.isNNRat_rpow_neg

deleted theorem Mathlib.Meta.NormNum.isNNRat_rpow_pos

deleted theorem Mathlib.Meta.NormNum.isNat_rpow_neg

deleted theorem Mathlib.Meta.NormNum.isNat_rpow_pos

deleted theorem Mathlib.Meta.NormNum.isRat_rpow_neg

deleted theorem Mathlib.Meta.NormNum.isRat_rpow_pos

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

deleted theorem Real.arctan_le_arctan

deleted theorem Real.arctan_lt_arctan

Modified Mathlib/Analysis/SpecificLimits/Basic.lean

Modified Mathlib/Analysis/SpecificLimits/RCLike.lean

Modified Mathlib/CategoryTheory/Abelian/Basic.lean

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

Modified Mathlib/CategoryTheory/Localization/Construction.lean

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

Modified Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean

Modified Mathlib/CategoryTheory/Monoidal/Linear.lean

Modified Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom_fst

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom_snd_fst

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom_snd_snd

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_inv

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_inv_fst_fst

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_inv_fst_snd

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_inv_snd

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.leftUnitor_hom

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.rightUnitor_hom

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.tensorObj

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.tensorUnit

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.tensor_ext

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.unit_ext

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.δ_eq

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.η_eq

deleted def CategoryTheory.monoidalOfHasFiniteProducts

deleted def CategoryTheory.symmetricOfHasFiniteProducts

Modified Mathlib/CategoryTheory/Monoidal/Rigid/OfEquivalence.lean

Modified Mathlib/CategoryTheory/Shift/CommShift.lean

Modified Mathlib/CategoryTheory/Sites/Canonical.lean

Modified Mathlib/CategoryTheory/Sites/Subcanonical.lean

Modified Mathlib/CategoryTheory/Yoneda.lean

deleted def CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight

deleted def CategoryTheory.Functor.FullyFaithful.homNatIsoMaxRight

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

deleted theorem SimpleGraph.Subgraph.Connected.adj_union

deleted theorem SimpleGraph.induce_connected_adj_union

Modified Mathlib/Combinatorics/SimpleGraph/Paths.lean

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

Modified Mathlib/Computability/Language.lean

deleted theorem Language.le_add_congr

deleted theorem Language.le_mul_congr

Modified Mathlib/Data/Array/Extract.lean

Modified Mathlib/Data/ENNReal/Inv.lean

Modified Mathlib/Data/ENNReal/Operations.lean

Modified Mathlib/Data/ENNReal/Real.lean

deleted theorem ENNReal.sup_eq_zero

Modified Mathlib/Data/Finset/Defs.lean

Modified Mathlib/Data/Finsupp/Lex.lean

deleted theorem Finsupp.Lex.single_antitone

Modified Mathlib/Data/Finsupp/PWO.lean

deleted theorem Finsupp.isPWO

Modified Mathlib/Data/Fintype/Sets.lean

Modified Mathlib/Data/Int/GCD.lean

Modified Mathlib/Data/Int/ModEq.lean

deleted theorem Int.modEq_add_fac

deleted theorem Int.modEq_sub_fac

Modified Mathlib/Data/List/Chain.lean

Modified Mathlib/Data/List/FinRange.lean

Modified Mathlib/Data/List/Nodup.lean

deleted theorem List.idxOf_getElem

Modified Mathlib/Data/Nat/Factorial/Basic.lean

deleted theorem Nat.factorialBinarySplitting.factorial_mul_prodRange

deleted def Nat.factorialBinarySplitting.prodRange

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

Modified Mathlib/Data/Nat/ModEq.lean

Modified Mathlib/Data/PNat/Prime.lean

Modified Mathlib/Data/Rat/Defs.lean

Modified Mathlib/Data/Set/Function.lean

deleted theorem Set.bijective_iff_bijOn_univ

deleted theorem Set.injective_iff_injOn_univ

deleted theorem Set.surjective_iff_surjOn_univ

Modified Mathlib/Data/String/Basic.lean

deleted theorem List.asString_eq

deleted theorem List.toList_asString

deleted theorem String.asString_nil

deleted theorem String.asString_toList

Modified Mathlib/Data/Sym/Sym2.lean

deleted theorem Sym2.isDiag_iff_mem_range_diag

deleted theorem Sym2.mem_diagSet_iff_eq

Modified Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean

deleted theorem Dynamics.idRel_subset_dynEntourage

deleted theorem IsSymmetricRel.dynEntourage

Modified Mathlib/FieldTheory/NormalizedTrace.lean

Modified Mathlib/GroupTheory/GroupAction/Jordan.lean

Modified Mathlib/GroupTheory/QuotientGroup/Basic.lean

Modified Mathlib/GroupTheory/QuotientGroup/Finite.lean

Modified Mathlib/LinearAlgebra/Basis/Flag.lean

deleted theorem Module.Basis.flag_le_flag

deleted theorem Module.Basis.flag_lt_flag

Modified Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Basic.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Defs.lean

deleted theorem LinearIndepOn.id_singleton

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

Modified Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/FinTwo.lean

Modified Mathlib/LinearAlgebra/Matrix/Hermitian.lean

Modified Mathlib/LinearAlgebra/Matrix/Notation.lean

Modified Mathlib/LinearAlgebra/Quotient/Basic.lean

deleted theorem Submodule.Quotient.nontrivial_of_lt_top

deleted theorem Submodule.Quotient.nontrivial_of_ne_top

Modified Mathlib/Logic/Equiv/Set.lean

deleted theorem Set.image_equiv_eq_preimage_symm

deleted theorem Set.preimage_equiv_eq_image_symm

Modified Mathlib/Logic/Equiv/Sum.lean

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

Modified Mathlib/MeasureTheory/Group/Arithmetic.lean

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

deleted theorem EuclideanSpace.coe_measurableEquiv

deleted theorem EuclideanSpace.coe_measurableEquiv_symm

deleted theorem EuclideanSpace.measurableEquiv_toEquiv

Modified Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean

Modified Mathlib/NumberTheory/LSeries/PrimesInAP.lean

Modified Mathlib/NumberTheory/Niven.lean

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

Modified Mathlib/NumberTheory/RamificationInertia/Galois.lean

Modified Mathlib/Order/Basic.lean

deleted def AsLinearOrder

Modified Mathlib/Order/Cover.lean

Modified Mathlib/Order/Disjoint.lean

deleted theorem Codisjoint.ne_bot_of_ne_top'

Modified Mathlib/Order/Filter/CardinalInter.lean

Modified Mathlib/Order/Interval/Set/OrdConnected.lean

Modified Mathlib/Order/Interval/Set/UnorderedInterval.lean

deleted theorem Set.uIoo_subset_uIcc

Modified Mathlib/Order/WellFoundedSet.lean

deleted theorem Pi.isPWO

Modified Mathlib/Probability/Independence/Basic.lean

Modified Mathlib/Probability/Independence/Conditional.lean

Modified Mathlib/Probability/Independence/Kernel/Indep.lean

Modified Mathlib/Probability/Martingale/BorelCantelli.lean

Modified Mathlib/Probability/Martingale/OptionalStopping.lean

Modified Mathlib/Probability/Process/HittingTime.lean

Modified Mathlib/RingTheory/Etale/Basic.lean

Modified Mathlib/RingTheory/Ideal/GoingUp.lean

Modified Mathlib/RingTheory/Ideal/Quotient/Basic.lean

Modified Mathlib/RingTheory/LaurentSeries.lean

deleted theorem RatFunc.single_inv

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

Modified Mathlib/RingTheory/Nilpotent/Basic.lean

deleted theorem NoZeroSMulDivisors.isReduced

Modified Mathlib/RingTheory/Polynomial/Resultant/Basic.lean

Modified Mathlib/RingTheory/PowerSeries/Order.lean

deleted theorem PowerSeries.divXPowOrder_mul_divXPowOrder

Modified Mathlib/RingTheory/Radical/Basic.lean

deleted theorem UniqueFactorizationMonoid.radical_eq_of_primeFactors_eq

Modified Mathlib/RingTheory/Smooth/Basic.lean

Modified Mathlib/RingTheory/Trace/Basic.lean

Modified Mathlib/RingTheory/Unramified/Basic.lean

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

Modified Mathlib/SetTheory/Ordinal/Basic.lean

Modified Mathlib/SetTheory/Ordinal/FixedPoint.lean

deleted theorem Ordinal.fp_iff_deriv

Modified Mathlib/SetTheory/ZFC/Basic.lean

deleted theorem ZFSet.mem_toSet

deleted theorem ZFSet.toSet_inj

deleted theorem ZFSet.toSet_injective

Modified Mathlib/SetTheory/ZFC/Class.lean

Modified Mathlib/Topology/ContinuousMap/Bounded/Basic.lean

Modified Mathlib/Topology/ContinuousMap/CompactlySupported.lean

Modified Mathlib/Topology/Homotopy/Path.lean

Modified Mathlib/Topology/KrullDimension.lean

Modified Mathlib/Topology/MetricSpace/BundledFun.lean

Modified Mathlib/Topology/Path.lean

deleted theorem Path.symm_cast

deleted theorem Path.trans_cast

Modified Mathlib/Topology/Sets/Compacts.lean

Modified Mathlib/Topology/UniformSpace/Defs.lean

deleted theorem IsSymmetricRel.eq

deleted theorem IsSymmetricRel.iInter

deleted theorem IsSymmetricRel.image_prodMap

deleted theorem IsSymmetricRel.inter

deleted theorem IsSymmetricRel.mem_filter_prod_comm

deleted theorem IsSymmetricRel.mk_mem_comm

deleted theorem IsSymmetricRel.preimage_prodMap

deleted theorem IsSymmetricRel.prod_subset_comm

deleted theorem IsSymmetricRel.sInter

deleted def IsSymmetricRel

deleted theorem Monotone.compRel

deleted def compRel

deleted theorem compRel_assoc

deleted theorem eq_singleton_left_of_prod_subset_idRel

deleted theorem eq_singleton_right_prod_subset_idRel

deleted def idRel

deleted theorem idRel_subset

deleted theorem id_compRel

deleted theorem isSymmetricRel_idRel

deleted theorem isSymmetricRel_univ

deleted theorem left_subset_compRel

deleted theorem mem_compRel

deleted theorem mem_idRel

deleted theorem right_subset_compRel

deleted theorem subset_comp_self

deleted theorem subset_iterate_compRel

deleted theorem swap_idRel

deleted theorem symmetric_symmetrizeRel

deleted def symmetrizeRel

deleted theorem symmetrizeRel_subset_self

deleted theorem symmetrize_mono

Modified Mathlib/Topology/UniformSpace/DiscreteUniformity.lean

Modified Mathlib/Topology/UniformSpace/Ultra/Basic.lean

deleted theorem IsTransitiveRel.comp_eq_of_idRel_subset

deleted theorem IsTransitiveRel.comp_subset_self

deleted theorem IsTransitiveRel.iInter

deleted theorem IsTransitiveRel.inter

deleted theorem IsTransitiveRel.preimage_prodMap

deleted theorem IsTransitiveRel.sInter

deleted theorem IsTransitiveRel.symmetrizeRel

deleted def IsTransitiveRel

deleted theorem isTransitiveRel_empty

deleted theorem isTransitiveRel_iff_comp_subset_self

deleted theorem isTransitiveRel_singleton

deleted theorem isTransitiveRel_univ

Modified Mathlib/Topology/UniformSpace/Ultra/Completion.lean

Modified Mathlib/Topology/UniformSpace/Ultra/Constructions.lean