Commit 2025-01-06 10:15 886b3402

View on Github →

chore: remove >9 month old deprecations (#20505)

Estimated changes

Modified Mathlib/Algebra/Algebra/Operations.lean

Modified Mathlib/Algebra/Associated/Basic.lean

Modified Mathlib/Algebra/CharP/Reduced.lean

Modified Mathlib/Algebra/GCDMonoid/Basic.lean

Modified Mathlib/Algebra/Group/Basic.lean

deleted theorem exists_pow_eq_one_of_zpow_eq_one

Modified Mathlib/Algebra/Group/Defs.lean

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

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

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

deleted theorem div_mul_left

deleted theorem div_mul_right

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

deleted theorem Submodule.set_smul_mono_right

Modified Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

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

deleted theorem div_le_div_of_le

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

Modified Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean

Modified Mathlib/Algebra/Polynomial/Div.lean

Modified Mathlib/Algebra/Squarefree/Basic.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

Modified Mathlib/Analysis/CStarAlgebra/Matrix.lean

Modified Mathlib/Analysis/CStarAlgebra/Unitization.lean

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

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

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

Modified Mathlib/Analysis/Calculus/MeanValue.lean

Modified Mathlib/Analysis/Complex/Polynomial/Basic.lean

Modified Mathlib/Analysis/Fourier/FourierTransform.lean

Modified Mathlib/Analysis/InnerProductSpace/LaxMilgram.lean

Modified Mathlib/Analysis/InnerProductSpace/TwoDim.lean

Modified Mathlib/Analysis/LocallyConvex/Basic.lean

deleted theorem Absorbent.zero_mem'

deleted theorem balanced_zero_union_interior

Modified Mathlib/Analysis/Matrix.lean

Modified Mathlib/Analysis/Normed/Lp/LpEquiv.lean

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

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

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

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/Completeness.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/Mul.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean

Modified Mathlib/Analysis/NormedSpace/RCLike.lean

Modified Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean

Modified Mathlib/CategoryTheory/Filtered/Basic.lean

Modified Mathlib/CategoryTheory/IsConnected.lean

Modified Mathlib/CategoryTheory/Limits/FullSubcategory.lean

Modified Mathlib/CategoryTheory/Limits/Opposites.lean

Modified Mathlib/Combinatorics/SimpleGraph/Coloring.lean

deleted theorem SimpleGraph.chromaticNumber_le_card

Modified Mathlib/Data/Complex/Abs.lean

deleted theorem Complex.int_cast_abs

Modified Mathlib/Data/Countable/Small.lean

Modified Mathlib/Data/Fin/Basic.lean

deleted theorem Fin.eq_iff_veq

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/Data/Finset/Empty.lean

Modified Mathlib/Data/Finset/Lattice/Basic.lean

Modified Mathlib/Data/Int/Defs.lean

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.bind_ret_eq_map

Modified Mathlib/Data/List/Defs.lean

Modified Mathlib/Data/List/Infix.lean

Modified Mathlib/Data/List/Pairwise.lean

deleted theorem List.pairwise_map'

Modified Mathlib/Data/List/Sublists.lean

deleted theorem List.map_ret_sublist_sublists

Modified Mathlib/Data/NNReal/Defs.lean

Modified Mathlib/Data/Nat/Cast/Order/Basic.lean

deleted theorem Nat.cast_le_cast

Modified Mathlib/Data/Nat/Digits.lean

Modified Mathlib/Data/Rat/Cast/Defs.lean

Modified Mathlib/Data/Rat/Defs.lean

deleted theorem Rat.add_def''

deleted theorem Rat.divInt_neg_one_one

deleted theorem Rat.divInt_zero_one

deleted theorem Rat.sub_def''

Modified Mathlib/Data/Real/Sqrt.lean

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/Data/Set/Image.lean

deleted theorem Set.mem_image_elim

deleted theorem Set.mem_image_elim_on

deleted theorem Set.mem_image_iff_bex

Modified Mathlib/Data/ZMod/Quotient.lean

Modified Mathlib/Deprecated/Cardinal/PartENat.lean

Modified Mathlib/Deprecated/Submonoid.lean

Modified Mathlib/FieldTheory/PrimitiveElement.lean

Modified Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean

Modified Mathlib/Logic/Basic.lean

deleted theorem ball_of_forall

deleted theorem forall_of_ball

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean

Modified Mathlib/MeasureTheory/Function/L1Space.lean

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

deleted theorem MeasureTheory.stronglyMeasurable_of_isEmpty

Modified Mathlib/MeasureTheory/Integral/PeakFunction.lean

Modified Mathlib/MeasureTheory/Integral/SetToL1.lean

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

Modified Mathlib/NumberTheory/LSeries/Dirichlet.lean

Modified Mathlib/NumberTheory/Transcendental/Liouville/Residual.lean

Modified Mathlib/RingTheory/Flat/Basic.lean

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

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

Modified Mathlib/RingTheory/PowerBasis.lean

Modified Mathlib/RingTheory/PrincipalIdealDomain.lean

Modified Mathlib/RingTheory/SimpleModule.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean

deleted theorem ufm_of_gcd_of_wfDvdMonoid

Modified Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean

deleted theorem UniqueFactorizationMonoid.max_power_factor

Modified Mathlib/SetTheory/Cardinal/Arithmetic.lean

Modified Mathlib/SetTheory/Cardinal/ToNat.lean

deleted theorem Cardinal.toNat_finset_prod

deleted theorem Cardinal.toNat_le_of_le_of_lt_aleph0

deleted theorem Cardinal.toNat_lt_of_lt_of_lt_aleph0

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

Modified Mathlib/Topology/Algebra/UniformRing.lean

deleted theorem UniformSpace.ring_sep_quot

Modified Mathlib/Topology/Bases.lean

Modified Mathlib/Topology/CompactOpen.lean

deleted theorem ContinuousMap.continuous_curry'

deleted def ContinuousMap.curry'

Modified Mathlib/Topology/Compactness/Compact.lean

deleted theorem Filter.mem_coclosedCompact

deleted theorem Filter.mem_coclosed_compact'

Modified Mathlib/Topology/Constructions.lean

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

Modified Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean

Modified Mathlib/Topology/GDelta/Basic.lean

Modified Mathlib/Topology/GDelta/UniformSpace.lean

Modified Mathlib/Topology/Instances/Discrete.lean

deleted theorem DiscreteTopology.secondCountableTopology_of_encodable

Modified Mathlib/Topology/Instances/Int.lean

Modified Mathlib/Topology/Instances/Irrational.lean

Modified Mathlib/Topology/Instances/Real.lean

Modified Mathlib/Topology/Maps/Basic.lean

Modified Mathlib/Topology/MetricSpace/Completion.lean

Modified Mathlib/Topology/MetricSpace/Polish.lean

deleted theorem PolishSpace.t2Space

Modified Mathlib/Topology/MetricSpace/Sequences.lean

Modified Mathlib/Topology/Order.lean

deleted theorem nhdsAdjoint_nhds_of_ne

Modified Mathlib/Topology/Order/Basic.lean

deleted theorem atBot_le_nhds_bot

deleted theorem atTop_le_nhds_top

Modified Mathlib/Topology/Order/OrderClosed.lean

deleted theorem ClosedIciTopology.isClosed_ge'

deleted theorem ClosedIicTopology.isClosed_le'

Modified Mathlib/Topology/Semicontinuous.lean

Modified Mathlib/Topology/Separation/GDelta.lean

Modified Mathlib/Topology/Separation/Hausdorff.lean

Modified Mathlib/Topology/Separation/Regular.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

deleted def UniformSpace.ofNhdsEqComap

Modified Mathlib/Topology/UnitInterval.lean