Commit 2025-03-04 03:24 7dac5d03

View on Github →

chore: remove >6 month old deprecations (#22473)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Equiv.lean

Modified Mathlib/Algebra/Algebra/Subalgebra/IsSimpleOrder.lean

Modified Mathlib/Algebra/BigOperators/WithTop.lean

deleted theorem WithBot.prod_lt_bot

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

Modified Mathlib/Algebra/Group/Basic.lean

Modified Mathlib/Algebra/Group/Defs.lean

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

Modified Mathlib/Algebra/Group/Even.lean

Modified Mathlib/Algebra/GroupWithZero/Invertible.lean

Modified Mathlib/Algebra/Order/Floor.lean

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

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

Modified Mathlib/Algebra/Ring/Int/Parity.lean

deleted theorem Int.even_iff_not_odd

deleted theorem Int.odd_iff_not_even

Modified Mathlib/Algebra/Ring/Parity.lean

deleted theorem Nat.even_iff_not_odd

deleted theorem Nat.odd_iff_not_even

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

Modified Mathlib/Algebra/Ring/SumsOfSquares.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean

Modified Mathlib/Analysis/CStarAlgebra/Basic.lean

Modified Mathlib/Analysis/CStarAlgebra/Module/Defs.lean

Modified Mathlib/Analysis/Complex/Basic.lean

Modified Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean

Modified Mathlib/Analysis/Convex/Jensen.lean

Modified Mathlib/Analysis/Normed/Group/Uniform.lean

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

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

Modified Mathlib/Control/LawfulFix.lean

deleted theorem LawfulFix.fix_eq'

Modified Mathlib/Data/Bool/AllAny.lean

Modified Mathlib/Data/Complex/Norm.lean

Modified Mathlib/Data/ENNReal/Operations.lean

Modified Mathlib/Data/Fin/Basic.lean

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.erase_get

deleted theorem List.get_cons

Modified Mathlib/Data/List/Defs.lean

deleted theorem List.mem_cons_eq

deleted theorem List.not_exists_mem_nil

Modified Mathlib/Data/List/FinRange.lean

Modified Mathlib/Data/List/Flatten.lean

deleted theorem List.sublist_join

Modified Mathlib/Data/List/GetD.lean

deleted theorem List.getD_eq_get

deleted theorem List.getI_eq_get

Modified Mathlib/Data/List/Indexes.lean

Modified Mathlib/Data/List/Infix.lean

deleted theorem List.IsPrefix.get_eq

deleted theorem List.cons_prefix_iff

deleted theorem List.eq_of_infix_of_length_eq

deleted theorem List.eq_of_prefix_of_length_eq

deleted theorem List.eq_of_suffix_of_length_eq

Modified Mathlib/Data/List/Iterate.lean

deleted theorem List.get?_iterate

deleted theorem List.get_iterate

Modified Mathlib/Data/List/Lemmas.lean

Modified Mathlib/Data/List/Lex.lean

Modified Mathlib/Data/List/Range.lean

Modified Mathlib/Data/List/Rotate.lean

Modified Mathlib/Data/List/Scan.lean

deleted theorem List.get_succ_scanl

Modified Mathlib/Data/List/SplitOn.lean

Modified Mathlib/Data/List/TakeWhile.lean

Deleted Mathlib/Data/MLList/Dedup.lean

deleted def MLList.dedup

deleted def MLList.dedupBy

Deleted Mathlib/Data/MLList/DepthFirst.lean

deleted def depthFirst

deleted def depthFirstRemovingDuplicates'

deleted def depthFirstRemovingDuplicates

Deleted Mathlib/Data/MLList/IO.lean

deleted def MLList.lines

deleted def MLList.linesFromHandle

deleted def MLList.runCmd

Deleted Mathlib/Data/MLList/Split.lean

deleted def MLList.getUpToFirst

deleted def MLList.groupBy

deleted def MLList.splitAtBecomesTrue

deleted def MLList.splitWhile

Modified Mathlib/Data/Matrix/Basis.lean

deleted theorem Matrix.std_basis_eq_basis_mul_basis

Modified Mathlib/Data/NNReal/Defs.lean

deleted theorem NNReal.le_div_iff_mul_le

deleted theorem NNReal.mul_le_iff_le_inv

Modified Mathlib/Data/Nat/Init.lean

deleted theorem Nat.one_mod_of_ne_one

Modified Mathlib/Data/Quot.lean

Modified Mathlib/Data/Real/Basic.lean

Modified Mathlib/Data/Real/Sqrt.lean

deleted theorem Real.sqrt_eq_iff_eq_mul_self

deleted theorem Real.sqrt_eq_iff_sq_eq

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/Data/Setoid/Basic.lean

Deleted Mathlib/Deprecated/ByteArray.lean

deleted def ByteArray.toSlice

deleted def ByteArray.toSliceT

deleted def ByteSlice.forIn.loop

deleted def ByteSlice.getOp

deleted def ByteSlice.toArray

deleted def ByteSlice.toString

deleted structure ByteSlice

deleted def ByteSliceT.getOp

deleted def ByteSliceT.size

deleted def ByteSliceT.toSlice

deleted structure ByteSliceT

deleted theorem Nat.Up.WF

deleted theorem Nat.Up.next

deleted def Nat.Up

deleted def Nat.upRel

Deleted Mathlib/Deprecated/NatLemmas.lean

deleted def Nat.discriminate

Modified Mathlib/Dynamics/Ergodic/MeasurePreserving.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

Modified Mathlib/FieldTheory/PerfectClosure.lean

Modified Mathlib/FieldTheory/Separable.lean

Modified Mathlib/GroupTheory/Coset/Defs.lean

Modified Mathlib/GroupTheory/Perm/List.lean

deleted theorem List.formPerm_apply_get

deleted theorem List.formPerm_apply_get_length

deleted theorem List.formPerm_apply_get_zero

deleted theorem List.formPerm_apply_lt_get

deleted theorem List.formPerm_pow_apply_get

Modified Mathlib/LinearAlgebra/Basis/Defs.lean

Modified Mathlib/LinearAlgebra/Dual.lean

Modified Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean

Modified Mathlib/LinearAlgebra/Finsupp/VectorSpace.lean

deleted theorem Basis.equivFun_symm_stdBasis

Modified Mathlib/LinearAlgebra/FreeModule/Basic.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Basic.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Defs.lean

Modified Mathlib/LinearAlgebra/Matrix/BilinearForm.lean

deleted theorem Matrix.toBilin'_stdBasis

Modified Mathlib/LinearAlgebra/Matrix/Diagonal.lean

deleted theorem Matrix.diagonal_comp_stdBasis

Modified Mathlib/LinearAlgebra/Matrix/DotProduct.lean

deleted theorem dotProduct_stdBasis_eq_mul

deleted theorem dotProduct_stdBasis_one

Modified Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean

deleted theorem Matrix.toLinearMap₂'_stdBasis

deleted theorem Matrix.toLinearMapₛₗ₂'_stdBasis

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

deleted theorem Matrix.mulVec_stdBasis

deleted theorem Matrix.mulVec_stdBasis_apply

deleted theorem Matrix.vecMul_stdBasis

Modified Mathlib/LinearAlgebra/Matrix/Transvection.lean

deleted theorem Matrix.Pivot.listTransvecCol_get

deleted theorem Matrix.Pivot.listTransvecRow_get

Modified Mathlib/LinearAlgebra/Quotient/Defs.lean

Modified Mathlib/LinearAlgebra/StdBasis.lean

deleted theorem LinearMap.coe_stdBasis

deleted theorem LinearMap.disjoint_stdBasis_stdBasis

deleted theorem LinearMap.iInf_ker_proj_le_iSup_range_stdBasis

deleted theorem LinearMap.iSup_range_stdBasis

deleted theorem LinearMap.iSup_range_stdBasis_eq_iInf_ker_proj

deleted theorem LinearMap.iSup_range_stdBasis_le_iInf_ker_proj

deleted theorem LinearMap.ker_stdBasis

deleted theorem LinearMap.proj_comp_stdBasis

deleted theorem LinearMap.proj_stdBasis_ne

deleted theorem LinearMap.proj_stdBasis_same

deleted def LinearMap.stdBasis

deleted theorem LinearMap.stdBasis_apply'

deleted theorem LinearMap.stdBasis_apply

deleted theorem LinearMap.stdBasis_eq_pi_diag

deleted theorem LinearMap.stdBasis_eq_single

deleted theorem LinearMap.stdBasis_ne

deleted theorem LinearMap.stdBasis_same

deleted theorem Pi.basis_repr_stdBasis

deleted theorem Pi.linearIndependent_stdBasis

Modified Mathlib/Logic/Nonempty.lean

Modified Mathlib/Logic/Relation.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Card.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Defs.lean

deleted theorem measurableSet_discrete

deleted theorem measurable_discrete

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

deleted theorem MeasureTheory.exists_absolutelyContinuous_isFiniteMeasure

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

Modified Mathlib/Order/Defs/LinearOrder.lean

Modified Mathlib/Order/Filter/Basic.lean

Modified Mathlib/Order/Filter/Pointwise.lean

Modified Mathlib/Order/LiminfLimsup.lean

Modified Mathlib/Probability/Kernel/Composition/CompProd.lean

Modified Mathlib/RingTheory/Kaehler/Basic.lean

Modified Mathlib/RingTheory/MatrixAlgebra.lean

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

deleted def Cardinal.Aleph'.relIso

deleted theorem Cardinal.aleph'.relIso_coe

deleted def Cardinal.aleph'Equiv

deleted theorem Cardinal.aleph'_alephIdx

deleted def Cardinal.alephIdx.initialSeg

deleted def Cardinal.alephIdx.relIso

deleted theorem Cardinal.alephIdx.relIso_coe

deleted def Cardinal.alephIdx

deleted theorem Cardinal.alephIdx_aleph'

deleted theorem Cardinal.max_aleph_eq

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

deleted theorem Cardinal.sup_lt_ord_lift_of_isRegular

deleted theorem Cardinal.sup_lt_ord_of_isRegular

deleted theorem Ordinal.cof_sup_le

deleted theorem Ordinal.cof_sup_le_lift

deleted theorem Ordinal.sup_lt_ord

deleted theorem Ordinal.sup_lt_ord_lift

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

deleted theorem Ordinal.le_sup_shrink_equiv

deleted theorem Ordinal.lt_sup

deleted theorem Ordinal.sSup_eq_sup

deleted theorem Ordinal.sup_add_nat

deleted theorem Ordinal.sup_empty

deleted theorem Ordinal.sup_eq_sSup

deleted theorem Ordinal.sup_eq_zero_iff

deleted theorem Ordinal.sup_mul_nat

deleted theorem Ordinal.unbounded_range_of_sup_ge

Modified Mathlib/SetTheory/Ordinal/Basic.lean

deleted theorem Ordinal.eq_zero_of_out_empty

deleted theorem Ordinal.ne_zero_of_out_nonempty

deleted theorem Ordinal.type_out

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

deleted theorem Ordinal.sup_opow_nat

Modified Mathlib/SetTheory/Ordinal/FixedPoint.lean

deleted theorem Ordinal.sup_iterate_eq_nfp

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean

Modified Mathlib/SetTheory/Ordinal/Principal.lean

deleted theorem Ordinal.principal_iff_principal_swap

Modified Mathlib/SetTheory/Ordinal/Topology.lean

deleted theorem Ordinal.isClosed_iff_sup

deleted theorem Ordinal.mem_closed_iff_sup

deleted theorem Ordinal.mem_closure_iff_sup

Modified Mathlib/Topology/Algebra/ConstMulAction.lean

deleted theorem set_smul_mem_nhds_smul

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

deleted theorem QuotientGroup.nhds_one_isCountablyGenerated

deleted theorem topologicalGroup_quotient

Modified Mathlib/Topology/Order/Monotone.lean