Commit 2025-04-01 02:20 3f6cf10f

View on Github →

chore: remove >6 month old deprecations (2024-09) (#23516) I may want to remove deprecations every 10 days so as to keep the diffs small.

Estimated changes

Modified Mathlib.lean

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

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

Modified Mathlib/Algebra/Group/Pointwise/Set/Card.lean

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

Modified Mathlib/Algebra/Lie/Weights/RootSystem.lean

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

Deleted Mathlib/Algebra/Order/Floor/Prime.lean

deleted theorem FloorRing.exists_prime_mul_pow_div_factorial_lt_one

deleted theorem FloorRing.exists_prime_mul_pow_lt_factorial

deleted theorem Nat.exists_prime_mul_pow_lt_factorial

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

Modified Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean

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

Modified Mathlib/Algebra/Prime/Lemmas.lean

Modified Mathlib/Algebra/Star/SelfAdjoint.lean

Modified Mathlib/Algebra/Star/StarAlgHom.lean

Modified Mathlib/Analysis/Analytic/Basic.lean

Modified Mathlib/Analysis/Analytic/CPolynomial.lean

Modified Mathlib/Analysis/Analytic/ChangeOrigin.lean

Modified Mathlib/Analysis/Analytic/Composition.lean

Modified Mathlib/Analysis/Analytic/Constructions.lean

Modified Mathlib/Analysis/Analytic/IsolatedZeros.lean

Modified Mathlib/Analysis/Analytic/Linear.lean

Modified Mathlib/Analysis/Analytic/Polynomial.lean

Modified Mathlib/Analysis/Analytic/Within.lean

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

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

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

Modified Mathlib/Analysis/Complex/OpenMapping.lean

Modified Mathlib/Analysis/InnerProductSpace/Symmetric.lean

Modified Mathlib/Analysis/Meromorphic/Basic.lean

Modified Mathlib/Data/ENNReal/Operations.lean

deleted theorem ENNReal.sub_eq_of_add_eq

Modified Mathlib/Data/ENat/Basic.lean

deleted theorem ENat.add_one_le_of_lt

deleted theorem ENat.le_of_lt_add_one

deleted theorem ENat.one_le_iff_pos

Modified Mathlib/Data/Fin/Basic.lean

deleted theorem Fin.coe_fin_one

Modified Mathlib/Data/Fin/Tuple/Finset.lean

Modified Mathlib/Data/Finset/Insert.lean

Modified Mathlib/Data/Finset/NAry.lean

Modified Mathlib/Data/Fintype/Order.lean

Modified Mathlib/Data/Int/SuccPred.lean

deleted theorem Int.covBy_add_one

deleted theorem Int.pos_iff_one_le

deleted theorem Int.sub_one_covBy

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/List/MinMax.lean

Modified Mathlib/Data/List/Perm/Basic.lean

Modified Mathlib/Data/Matrix/Invertible.lean

Modified Mathlib/Data/Nat/Prime/Nth.lean

Modified Mathlib/Data/Nat/SuccPred.lean

Modified Mathlib/Data/Ordering/Basic.lean

Modified Mathlib/Data/Quot.lean

deleted theorem surjective_quot_mk

deleted theorem surjective_quotient_mk'

deleted theorem surjective_quotient_mk

Modified Mathlib/Data/Real/Pi/Bounds.lean

Modified Mathlib/Data/Set/Image.lean

Modified Mathlib/FieldTheory/RatFunc/Basic.lean

deleted theorem RatFunc.algebraMap_eq_zero_iff

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

Modified Mathlib/LinearAlgebra/Dimension/Basic.lean

Modified Mathlib/LinearAlgebra/Dimension/Constructions.lean

Modified Mathlib/Logic/Function/Defs.lean

Modified Mathlib/Logic/Relation.lean

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/MeasureTheory/OuterMeasure/BorelCantelli.lean

Modified Mathlib/MeasureTheory/VectorMeasure/Basic.lean

deleted theorem MeasureTheory.VectorMeasure.of_disjoint_iUnion_nat

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

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

deleted theorem Nat.exists_mul_pow_lt_factorial

deleted theorem Nat.exists_pow_lt_factorial

Modified Mathlib/Order/SuccPred/Limit.lean

Modified Mathlib/Probability/BorelCantelli.lean

Modified Mathlib/Probability/Martingale/BorelCantelli.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean

deleted theorem WfDvdMonoid.of_wellFounded_associates

deleted theorem WfDvdMonoid.wellFounded_associates

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

deleted theorem Cardinal.eq_aleph'_of_eq_card_ord

deleted theorem Cardinal.eq_aleph_of_eq_card_ord

deleted theorem Cardinal.ord_card_unbounded'

deleted theorem Cardinal.ord_card_unbounded

Modified Mathlib/SetTheory/Game/Ordinal.lean

deleted theorem Ordinal.toPGame_def

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

Modified Mathlib/SetTheory/Ordinal/Family.lean

Modified Mathlib/SetTheory/Ordinal/FixedPoint.lean

Modified Mathlib/SetTheory/Ordinal/Notation.lean

Modified Mathlib/SetTheory/Ordinal/Principal.lean

Modified Mathlib/SetTheory/PGame/Order.lean

Modified Mathlib/Topology/Basic.lean

deleted theorem mapClusterPt_of_comp

Modified Mathlib/Topology/Category/TopCat/Opens.lean

Modified Mathlib/Topology/Compactification/OnePoint.lean

Modified Mathlib/Topology/Compactness/Exterior.lean

deleted theorem Set.Finite.isCompact_exterior

Modified Mathlib/Topology/ContinuousMap/Defs.lean

deleted theorem ContinuousMap.continuous_set_coe

Modified Mathlib/Topology/DenseEmbedding.lean

Modified Mathlib/Topology/Exterior.lean

Modified Mathlib/Topology/Homeomorph/Lemmas.lean

Modified Mathlib/Topology/Instances/ENNReal/Lemmas.lean

deleted theorem ENNReal.iInf_mul_left'

deleted theorem ENNReal.iInf_mul_left

deleted theorem ENNReal.iInf_mul_right'

deleted theorem ENNReal.iInf_mul_right

deleted theorem ENNReal.inv_map_iInf

deleted theorem ENNReal.inv_map_iSup

deleted theorem ENNReal.ofReal_cinfi

Modified Mathlib/Topology/Instances/Rat.lean

Modified Mathlib/Topology/StoneCech.lean

Modified Mathlib/Topology/UniformSpace/Completion.lean

Modified Mathlib/Topology/UniformSpace/UniformEmbedding.lean

Modified MathlibTest/LibrarySearch/basic.lean

Modified docs/undergrad.yaml