Commit 2025-04-11 00:24 fba98fa5

View on Github →

chore: delete >6 month old deprecations (2024-10 01-10) (#23928) Deprecations were found with the regex 2024-10-(0[1-9]|10).

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean

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

Modified Mathlib/Algebra/Category/Ring/Constructions.lean

Modified Mathlib/Algebra/Category/Ring/Instances.lean

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

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

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

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

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

Modified Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean

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

deleted theorem div_le_of_nonneg_of_le_mul

deleted theorem div_le_one_of_le

deleted theorem div_lt_iff'

deleted theorem div_lt_iff

deleted theorem inv_le

deleted theorem inv_le_inv

deleted theorem inv_le_inv_of_le

deleted theorem inv_le_of_inv_le

deleted theorem inv_le_one

deleted theorem inv_le_one_iff

deleted theorem inv_lt

deleted theorem inv_lt_inv

deleted theorem inv_lt_inv_of_lt

deleted theorem inv_lt_of_inv_lt

deleted theorem inv_lt_one

deleted theorem inv_lt_one_iff

deleted theorem inv_lt_one_iff_of_pos

deleted theorem inv_mul_le_iff'

deleted theorem inv_mul_le_iff

deleted theorem inv_mul_le_one_of_le

deleted theorem inv_mul_lt_iff'

deleted theorem inv_mul_lt_iff

deleted theorem inv_pos_le_iff_one_le_mul'

deleted theorem inv_pos_le_iff_one_le_mul

deleted theorem inv_pos_lt_iff_one_lt_mul'

deleted theorem inv_pos_lt_iff_one_lt_mul

deleted theorem le_inv

deleted theorem lt_div_iff'

deleted theorem lt_div_iff

deleted theorem lt_inv

deleted theorem mul_inv_le_iff'

deleted theorem mul_inv_le_iff

deleted theorem mul_inv_le_one_of_le

deleted theorem mul_inv_lt_iff'

deleted theorem mul_inv_lt_iff

deleted theorem mul_le_of_nonneg_of_le_div

deleted theorem one_le_inv

deleted theorem one_le_inv_iff

deleted theorem one_lt_inv

deleted theorem one_lt_inv_iff

Modified Mathlib/Algebra/Order/Field/Power.lean

deleted theorem Nat.zpow_ne_zero_of_pos

deleted theorem div_pow_le

deleted theorem one_le_zpow_of_nonneg

deleted theorem zpow_inj

deleted theorem zpow_injective

deleted theorem zpow_le_iff_le

deleted theorem zpow_le_max_iff_min_le

deleted theorem zpow_le_max_of_min_le

deleted theorem zpow_le_of_le

deleted theorem zpow_le_one_of_nonpos

deleted theorem zpow_lt_iff_lt

deleted theorem zpow_strictAnti

deleted theorem zpow_strictMono

Modified Mathlib/Algebra/Order/GroupWithZero/Unbundled/Basic.lean

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

Modified Mathlib/Algebra/Polynomial/Expand.lean

Modified Mathlib/Algebra/Polynomial/Splits.lean

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

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

Modified Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

Modified Mathlib/Analysis/CStarAlgebra/Multiplier.lean

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

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

Modified Mathlib/Analysis/Complex/Basic.lean

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

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

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

Modified Mathlib/Analysis/ODE/PicardLindelof.lean

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

deleted theorem Real.tendsto_pow_div_factorial_atTop

Modified Mathlib/CategoryTheory/Adjunction/Unique.lean

Modified Mathlib/CategoryTheory/Yoneda.lean

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

Modified Mathlib/Data/Finset/Basic.lean

deleted theorem Finset.sdiff_singleton_eq_self

Modified Mathlib/Data/Finset/SDiff.lean

Modified Mathlib/Data/NNReal/Defs.lean

deleted theorem NNReal.div_lt_iff'

deleted theorem NNReal.div_lt_iff

deleted theorem NNReal.le_div_iff'

deleted theorem NNReal.lt_div_iff'

deleted theorem NNReal.lt_div_iff

Modified Mathlib/Data/Real/Archimedean.lean

Modified Mathlib/Data/Set/Piecewise.lean

Modified Mathlib/Data/Set/Prod.lean

Modified Mathlib/Data/Setoid/Basic.lean

deleted theorem Quotient.eq_rel

deleted def Setoid.Rel

deleted theorem Setoid.ext'

deleted theorem Setoid.ext'_iff

Modified Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

Modified Mathlib/Geometry/Manifold/MFDeriv/Defs.lean

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Combination.lean

Modified Mathlib/LinearAlgebra/Dimension/Basic.lean

Modified Mathlib/LinearAlgebra/Dimension/Finrank.lean

Modified Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

Modified Mathlib/LinearAlgebra/Span/Defs.lean

Modified Mathlib/Logic/Function/Basic.lean

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

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

Modified Mathlib/MeasureTheory/Measure/WithDensityFinite.lean

deleted theorem MeasureTheory.densityToFinite_ae_lt_top

deleted theorem MeasureTheory.densityToFinite_ae_ne_top

deleted theorem MeasureTheory.densityToFinite_def

deleted theorem MeasureTheory.measurable_densityToFinite

deleted theorem MeasureTheory.withDensity_densitytoFinite

Modified Mathlib/Order/CompactlyGenerated/Basic.lean

Modified Mathlib/Order/InitialSeg.lean

deleted theorem PrincipalSeg.down

Modified Mathlib/Probability/UniformOn.lean

Modified Mathlib/RingTheory/Henselian.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

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

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

Modified Mathlib/RingTheory/Localization/AtPrime.lean

Modified Mathlib/RingTheory/MvPowerSeries/Inverse.lean

Modified Mathlib/RingTheory/PowerSeries/Inverse.lean

Modified Mathlib/RingTheory/Spectrum/Prime/Topology.lean

Modified Mathlib/RingTheory/SurjectiveOnStalks.lean

Modified Mathlib/RingTheory/Valuation/ValExtension.lean

Modified Mathlib/SetTheory/Cardinal/Order.lean

deleted def Cardinal.liftOrderEmbedding

deleted theorem Cardinal.lift_down

Modified Mathlib/SetTheory/Ordinal/Basic.lean

deleted theorem Ordinal.lift_down'

deleted theorem Ordinal.lift_down

deleted theorem Ordinal.typein.principalSeg_coe

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

deleted theorem Ordinal.log_of_not_one_lt_left

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

deleted structure ContinuousAddMonoidHomClass

deleted structure ContinuousMonoidHomClass

Modified Mathlib/Topology/Algebra/Group/Quotient.lean

deleted theorem QuotientGroup.continuous_smul₁

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

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

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

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

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

Modified Mathlib/Topology/Algebra/SeparationQuotient/Section.lean

Modified Mathlib/Topology/Algebra/UniformMulAction.lean

Modified Mathlib/Topology/CompactOpen.lean

deleted theorem ContinuousMap.continuous_coe

Modified Mathlib/Topology/Constructions/SumProd.lean

Modified Mathlib/Topology/ContinuousMap/Compact.lean

Modified Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean

Modified Mathlib/Topology/ContinuousOn.lean

Modified Mathlib/Topology/DenseEmbedding.lean

Modified Mathlib/Topology/EMetricSpace/Basic.lean

Modified Mathlib/Topology/Instances/Int.lean

Modified Mathlib/Topology/Instances/Nat.lean

Modified Mathlib/Topology/Instances/PNat.lean

Modified Mathlib/Topology/Instances/Rat.lean

Modified Mathlib/Topology/Maps/Proper/Basic.lean

Modified Mathlib/Topology/MetricSpace/Antilipschitz.lean

Modified Mathlib/Topology/MetricSpace/Basic.lean

Modified Mathlib/Topology/MetricSpace/Closeds.lean

Modified Mathlib/Topology/MetricSpace/Dilation.lean

Modified Mathlib/Topology/MetricSpace/Isometry.lean

Modified Mathlib/Topology/MetricSpace/Pseudo/Basic.lean

Modified Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean

Modified Mathlib/Topology/Neighborhoods.lean

Modified Mathlib/Topology/NoetherianSpace.lean

deleted theorem TopologicalSpace.NoetherianSpace.wellFounded_closeds

Modified Mathlib/Topology/Order/UpperLowerSetTopology.lean

Modified Mathlib/Topology/Path.lean

deleted theorem Continuous.path_eval

Modified Mathlib/Topology/Sober.lean

Modified Mathlib/Topology/UniformSpace/AbstractCompletion.lean

Modified Mathlib/Topology/UniformSpace/Ascoli.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

Modified Mathlib/Topology/UniformSpace/CompactConvergence.lean

Modified Mathlib/Topology/UniformSpace/CompleteSeparated.lean

Modified Mathlib/Topology/UniformSpace/Completion.lean

Modified Mathlib/Topology/UniformSpace/Equicontinuity.lean

Modified Mathlib/Topology/UniformSpace/Equiv.lean

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

Modified Mathlib/Topology/UniformSpace/UniformEmbedding.lean