Commit 2026-04-17 09:59 d0818abc

View on Github →

chore: remove declarations deprecated between 2021-04-15 and 2025-10-15 (#38057) 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/Category/Grp/CartesianMonoidal.lean

Modified Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean

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

deleted theorem Subgroup.pi_mem_of_mulSingle_mem_aux

Modified Mathlib/Algebra/GroupWithZero/Basic.lean

Modified Mathlib/Algebra/Lie/Basic.lean

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

Modified Mathlib/Algebra/Polynomial/Splits.lean

Modified Mathlib/Algebra/Ring/Invertible.lean

Modified Mathlib/Algebra/Star/SelfAdjoint.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/AlgebraicGeometry/AffineSpace.lean

Modified Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean

Modified Mathlib/AlgebraicGeometry/Gluing.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Affine.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Descent.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Integral.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/LocalIso.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Proper.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean

Modified Mathlib/AlgebraicGeometry/PullbackCarrier.lean

Modified Mathlib/AlgebraicGeometry/Pullbacks.lean

Modified Mathlib/AlgebraicGeometry/ResidueField.lean

Modified Mathlib/AlgebraicGeometry/Restrict.lean

Modified Mathlib/AlgebraicGeometry/Scheme.lean

Modified Mathlib/AlgebraicGeometry/Spec.lean

Modified Mathlib/AlgebraicGeometry/Stalk.lean

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

Modified Mathlib/Analysis/CStarAlgebra/Basic.lean

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

Modified Mathlib/Analysis/Calculus/VectorField.lean

Modified Mathlib/Analysis/Complex/ValueDistribution/FirstMainTheorem.lean

Modified Mathlib/Analysis/Convex/BetweenList.lean

Modified Mathlib/Analysis/LocallyConvex/Polar.lean

Modified Mathlib/Analysis/Matrix/Order.lean

deleted theorem Matrix.PosDef.commute_iff

deleted theorem Matrix.PosDef.posDef_sqrt

deleted theorem Matrix.posDef_iff_eq_conjTranspose_mul_self

Modified Mathlib/CategoryTheory/Bicategory/Strict/Pseudofunctor.lean

Modified Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean

Modified Mathlib/CategoryTheory/Generator/Basic.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/Over/Connected.lean

Modified Mathlib/CategoryTheory/Monoidal/CommGrp_.lean

Modified Mathlib/CategoryTheory/Monoidal/Grp_.lean

Modified Mathlib/CategoryTheory/Presentable/CardinalFilteredPresentation.lean

Modified Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean

Modified Mathlib/CategoryTheory/Sites/IsSheafFor.lean

deleted def CategoryTheory.Presieve.FamilyOfElements.compPresheafMap

Modified Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean

Modified Mathlib/Combinatorics/SimpleGraph/Cayley.lean

Modified Mathlib/Data/DFinsupp/Lex.lean

deleted theorem DFinsupp.lt_of_forall_lt_of_lt

Modified Mathlib/Data/Fin/Basic.lean

Modified Mathlib/Data/Finite/Card.lean

Modified Mathlib/Data/Finset/Sort.lean

Modified Mathlib/Data/Finsupp/Lex.lean

deleted theorem Finsupp.lt_of_forall_lt_of_lt

Modified Mathlib/Data/Int/DivMod.lean

Modified Mathlib/Data/List/FinRange.lean

deleted theorem List.finRange_succ_eq_map

Modified Mathlib/Data/List/Nodup.lean

Modified Mathlib/Data/List/NodupEquivFin.lean

Modified Mathlib/Data/List/OfFn.lean

Modified Mathlib/Data/List/Pairwise.lean

Modified Mathlib/Data/List/Sort.lean

Modified Mathlib/Data/Multiset/Sort.lean

Modified Mathlib/Data/Nat/Bitwise.lean

deleted theorem Nat.xor_cancel_left

deleted theorem Nat.xor_cancel_right

deleted theorem Nat.xor_eq_zero

deleted theorem Nat.xor_ne_zero

Modified Mathlib/Data/Nat/Log.lean

deleted theorem Nat.le_pow_iff_clog_le

deleted theorem Nat.lt_pow_iff_log_lt

deleted theorem Nat.pow_le_iff_le_log

deleted theorem Nat.pow_lt_iff_lt_clog

Modified Mathlib/Data/Setoid/Basic.lean

Modified Mathlib/Dynamics/Flow.lean

Modified Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean

Modified Mathlib/GroupTheory/GroupAction/Defs.lean

Modified Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean

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

Modified Mathlib/GroupTheory/Perm/List.lean

Modified Mathlib/LinearAlgebra/Alternating/Uncurry/Fin.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean

Modified Mathlib/NumberTheory/SumTwoSquares.lean

Modified Mathlib/Order/BooleanAlgebra/Basic.lean

Modified Mathlib/Probability/Independence/Conditional.lean

Modified Mathlib/Probability/Moments/CovarianceBilinDual.lean

Modified Mathlib/RingTheory/Adjoin/PowerBasis.lean

Modified Mathlib/RingTheory/AdjoinRoot.lean

deleted theorem AdjoinRoot.coe_liftHom

deleted def AdjoinRoot.liftHom

deleted theorem AdjoinRoot.liftHom_eq_algHom

deleted theorem AdjoinRoot.liftHom_mk

deleted theorem AdjoinRoot.liftHom_of

deleted theorem AdjoinRoot.liftHom_root

Modified Mathlib/RingTheory/Artinian/Defs.lean

Modified Mathlib/RingTheory/LocalRing/Quotient.lean

Modified Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean

Modified Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean

Modified Mathlib/RingTheory/PrincipalIdealDomain.lean

deleted def nonPrincipals

deleted theorem nonPrincipals_def

deleted theorem nonPrincipals_eq_empty_iff

deleted theorem nonPrincipals_zorn

Modified Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean

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

Modified Mathlib/SetTheory/Cardinal/Finsupp.lean

Modified Mathlib/SetTheory/Ordinal/Family.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean

Modified Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean

deleted theorem topologicalGroup_is_uniform_of_compactSpace

Modified Mathlib/Topology/Algebra/IsUniformGroup/Defs.lean

Modified Mathlib/Topology/Algebra/OpenSubgroup.lean

deleted theorem Subgroup.discreteTopology

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

Modified Mathlib/Topology/DiscreteSubset.lean

Modified Mathlib/Topology/Homeomorph/Defs.lean

Modified Mathlib/Topology/Order.lean

deleted theorem forall_open_iff_discrete

deleted theorem singletons_open_iff_discrete

Modified Mathlib/Topology/Sets/Closeds.lean

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