Commit 2025-08-05 07:35 e2e37a5e

View on Github →

chore: further >6month old deprecations (#27799)

Estimated changes

Modified Mathlib/Algebra/AddTorsor/Basic.lean

Modified Mathlib/Algebra/Algebra/Basic.lean

Modified Mathlib/Algebra/Algebra/Bilinear.lean

deleted theorem LinearMap.mulLeft_injective

deleted theorem LinearMap.mulRight_injective

deleted theorem LinearMap.mul_injective

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/Algebra/Spectrum/Basic.lean

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

Modified Mathlib/Algebra/Algebra/Subalgebra/Pointwise.lean

Modified Mathlib/Algebra/AlgebraicCard.lean

Modified Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean

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

deleted theorem CommGrp.comp_def

deleted theorem Grp.comp_def

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

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

deleted theorem Semigrp.comp_def

Modified Mathlib/Algebra/CharP/Defs.lean

Modified Mathlib/Algebra/DirectSum/Module.lean

Modified Mathlib/Algebra/GradedMonoid.lean

Modified Mathlib/Algebra/GradedMulAction.lean

Modified Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean

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

Modified Mathlib/Algebra/Group/Even.lean

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

Modified Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

Modified Mathlib/Algebra/Group/Pointwise/Finset/Scalar.lean

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

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

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

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

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

Modified Mathlib/Algebra/GroupWithZero/Action/Pointwise/Set.lean

Modified Mathlib/Algebra/GroupWithZero/NeZero.lean

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

Modified Mathlib/Algebra/Lie/Abelian.lean

Modified Mathlib/Algebra/Lie/Basic.lean

Modified Mathlib/Algebra/Lie/Ideal.lean

Modified Mathlib/Algebra/Lie/InvariantForm.lean

Modified Mathlib/Algebra/Lie/Nilpotent.lean

deleted theorem LieModule.exists_lowerCentralSeries_eq_bot_of_isNilpotent

Modified Mathlib/Algebra/Lie/Subalgebra.lean

Modified Mathlib/Algebra/Lie/Submodule.lean

Modified Mathlib/Algebra/Lie/TensorProduct.lean

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

Modified Mathlib/Algebra/Module/FinitePresentation.lean

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

deleted def DistribMulActionHom.toLinearMap

deleted def DistribMulActionHom.toSemilinearMap

Modified Mathlib/Algebra/Module/LocalizedModule/Basic.lean

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

Modified Mathlib/Algebra/Module/Torsion.lean

Modified Mathlib/Algebra/MvPolynomial/Cardinal.lean

Modified Mathlib/Algebra/MvPolynomial/CommRing.lean

Modified Mathlib/Algebra/MvPolynomial/Degrees.lean

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

Modified Mathlib/Algebra/Order/Antidiag/Nat.lean

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

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

deleted theorem div_le_div

deleted theorem div_le_div_iff

deleted theorem div_le_div_left

deleted theorem div_le_div_right

deleted theorem div_lt_div'

deleted theorem div_lt_div

deleted theorem div_lt_div_iff

deleted theorem div_lt_div_left

deleted theorem div_lt_div_right

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

Modified Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean

Modified Mathlib/Algebra/Order/Group/Pointwise/Interval.lean

deleted theorem Set.preimage_neg_uIcc

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

deleted def OrderIso.mulLeft₀'

deleted theorem OrderIso.mulLeft₀'_symm

deleted def OrderIso.mulRight₀'

deleted theorem OrderIso.mulRight₀'_symm

deleted theorem div_le_div_left₀

deleted theorem div_le_div_right₀

deleted theorem mul_inv_le_of_le_mul

deleted theorem mul_lt_mul_of_lt_of_le₀

deleted theorem mul_lt_mul₀

deleted theorem pow_lt_pow_succ

Modified Mathlib/Algebra/Order/Monoid/ToMulBot.lean

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

deleted theorem WithTop.zero_lt_coe

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

deleted theorem le_of_pow_le_pow_left

deleted theorem lt_of_mul_self_lt_mul_self

deleted theorem lt_of_pow_lt_pow_left

deleted theorem lt_self_pow

deleted theorem one_le_sq_iff

deleted theorem one_lt_sq_iff

deleted theorem pow_le_pow_iff_left

deleted theorem pow_le_pow_iff_right

deleted theorem pow_le_pow_left

deleted theorem pow_left_strictMonoOn

deleted theorem pow_lt_pow_iff_left

deleted theorem pow_lt_pow_iff_right

deleted theorem pow_lt_pow_iff_right_of_lt_one

deleted theorem pow_lt_pow_left

deleted theorem pow_lt_pow_right

deleted theorem pow_lt_pow_right_of_lt_one

deleted theorem pow_lt_self_of_lt_one

deleted theorem pow_right_inj

deleted theorem pow_right_injective

deleted theorem pow_right_strictAnti

deleted theorem pow_right_strictMono

deleted theorem sq_eq_sq

deleted theorem sq_le_one_iff

deleted theorem sq_lt_one_iff

Modified Mathlib/Algebra/Pointwise/Stabilizer.lean

Modified Mathlib/Algebra/Polynomial/Cardinal.lean

Modified Mathlib/Algebra/Polynomial/Degree/Lemmas.lean

Modified Mathlib/Algebra/Polynomial/Div.lean

Modified Mathlib/Algebra/Ring/Equiv.lean

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

Modified Mathlib/Algebra/Ring/SumsOfSquares.lean

Modified Mathlib/Algebra/Squarefree/Basic.lean

Modified Mathlib/Algebra/Star/Basic.lean

Modified Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/Vertex/HVertexOperator.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/AlgebraicGeometry/Cover/Open.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Basic.lean

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

Modified Mathlib/AlgebraicGeometry/Scheme.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Boundary.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

Modified Mathlib/Analysis/Asymptotics/Theta.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

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

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

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

Modified Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean

Modified Mathlib/Analysis/Calculus/Rademacher.lean

Modified Mathlib/Analysis/Complex/Basic.lean

Modified Mathlib/Analysis/Complex/Convex.lean

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

Modified Mathlib/Analysis/Convex/Basic.lean

Modified Mathlib/Analysis/Convex/Deriv.lean

Modified Mathlib/Analysis/Convex/Exposed.lean

Modified Mathlib/Analysis/Convex/StrictConvexSpace.lean

Modified Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

Modified Mathlib/Analysis/Normed/Field/Basic.lean

Modified Mathlib/Analysis/Normed/Field/Lemmas.lean

Modified Mathlib/Analysis/Normed/Field/WithAbs.lean

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

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

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

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

Modified Mathlib/Analysis/Normed/Ring/WithAbs.lean

deleted theorem WithAbs.equiv_add

deleted theorem WithAbs.equiv_mul

deleted theorem WithAbs.equiv_neg

deleted theorem WithAbs.equiv_sub

deleted theorem WithAbs.equiv_symm_add

deleted theorem WithAbs.equiv_symm_mul

deleted theorem WithAbs.equiv_symm_neg

deleted theorem WithAbs.equiv_symm_sub

deleted theorem WithAbs.equiv_symm_zero

deleted theorem WithAbs.equiv_zero

deleted def WithAbs.ringEquiv

Modified Mathlib/Analysis/Normed/Unbundled/RingSeminorm.lean

deleted theorem MulRingNorm.apply_natAbs_eq

deleted def MulRingNorm.equiv

deleted theorem MulRingNorm.equiv_refl

deleted theorem MulRingNorm.equiv_symm

deleted theorem MulRingNorm.equiv_trans

deleted theorem MulRingNorm_nat_le_nat

deleted theorem mulRingNorm_sum_le_sum_mulRingNorm

Modified Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean

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

deleted theorem ContinuousMultilinearMap.opNorm_neg

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

Modified Mathlib/Analysis/NormedSpace/Pointwise.lean

Modified Mathlib/Analysis/NormedSpace/Real.lean

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart/Basic.lean

deleted theorem CFC.eq_negPart_iff

deleted theorem CFC.eq_posPart_iff

Modified Mathlib/Analysis/SpecialFunctions/Exp.lean

Modified Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

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

Modified Mathlib/CategoryTheory/Adjunction/Limits.lean

deleted theorem CategoryTheory.Adjunction.isEquivalenceReflectsColimits

deleted theorem CategoryTheory.Adjunction.isEquivalenceReflectsLimits

deleted theorem CategoryTheory.Adjunction.leftAdjointPreservesColimits

deleted theorem CategoryTheory.Adjunction.rightAdjointPreservesLimits

Modified Mathlib/CategoryTheory/Adjunction/Opposites.lean

Modified Mathlib/CategoryTheory/Limits/Creates.lean

deleted theorem CategoryTheory.preservesColimitOfCreatesColimitAndHasColimit

deleted theorem CategoryTheory.preservesColimitOfShapeOfCreatesColimitsOfShapeAndHasColimitsOfShape

deleted theorem CategoryTheory.preservesColimitsOfCreatesColimitsAndHasColimits

deleted theorem CategoryTheory.preservesLimitOfCreatesLimitAndHasLimit

deleted theorem CategoryTheory.preservesLimitOfShapeOfCreatesLimitsOfShapeAndHasLimitsOfShape

deleted theorem CategoryTheory.preservesLimitsOfCreatesLimitsAndHasLimits

Modified Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean

deleted theorem CategoryTheory.Limits.preservesColimitOfEvaluation

deleted theorem CategoryTheory.Limits.preservesLimitOfEvaluation

deleted theorem CategoryTheory.Limits.preservesLimitsOfEvaluation

deleted theorem CategoryTheory.Limits.preservesLimitsOfShapeOfEvaluation

Modified Mathlib/CategoryTheory/Limits/Opposites.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Basic.lean

deleted theorem CategoryTheory.Limits.PreservesColimitsOfSizeShrink

deleted theorem CategoryTheory.Limits.PreservesLimitsOfSizeShrink

deleted theorem CategoryTheory.Limits.compPreservesColimit

deleted theorem CategoryTheory.Limits.compPreservesColimits

deleted theorem CategoryTheory.Limits.compPreservesColimitsOfShape

deleted theorem CategoryTheory.Limits.compPreservesLimit

deleted theorem CategoryTheory.Limits.compPreservesLimits

deleted theorem CategoryTheory.Limits.compPreservesLimitsOfShape

deleted theorem CategoryTheory.Limits.compReflectsColimit

deleted theorem CategoryTheory.Limits.compReflectsColimits

deleted theorem CategoryTheory.Limits.compReflectsColimitsOfShape

deleted theorem CategoryTheory.Limits.compReflectsLimit

deleted theorem CategoryTheory.Limits.compReflectsLimits

deleted theorem CategoryTheory.Limits.compReflectsLimitsOfShape

deleted theorem CategoryTheory.Limits.fullyFaithfulReflectsColimits

deleted theorem CategoryTheory.Limits.fullyFaithfulReflectsLimits

deleted theorem CategoryTheory.Limits.idPreservesColimits

deleted theorem CategoryTheory.Limits.idPreservesLimits

deleted theorem CategoryTheory.Limits.idReflectsColimits

deleted theorem CategoryTheory.Limits.idReflectsLimits

deleted theorem CategoryTheory.Limits.preservesColimitOfIsoDiagram

deleted theorem CategoryTheory.Limits.preservesColimitOfNatIso

deleted theorem CategoryTheory.Limits.preservesColimitOfPreservesColimitCocone

deleted theorem CategoryTheory.Limits.preservesColimitOfReflectsOfPreserves

deleted theorem CategoryTheory.Limits.preservesColimitsOfNatIso

deleted theorem CategoryTheory.Limits.preservesColimitsOfReflectsOfPreserves

deleted theorem CategoryTheory.Limits.preservesColimitsOfShapeOfEquiv

deleted theorem CategoryTheory.Limits.preservesColimitsOfShapeOfNatIso

deleted theorem CategoryTheory.Limits.preservesColimitsOfShapeOfReflectsOfPreserves

deleted theorem CategoryTheory.Limits.preservesColimitsOfSizeOfUnivLE

deleted theorem CategoryTheory.Limits.preservesLimitOfIsoDiagram

deleted theorem CategoryTheory.Limits.preservesLimitOfNatIso

deleted theorem CategoryTheory.Limits.preservesLimitOfPreservesLimitCone

deleted theorem CategoryTheory.Limits.preservesLimitOfReflectsOfPreserves

deleted theorem CategoryTheory.Limits.preservesLimitsOfNatIso

deleted theorem CategoryTheory.Limits.preservesLimitsOfReflectsOfPreserves

deleted theorem CategoryTheory.Limits.preservesLimitsOfShapeOfEquiv

deleted theorem CategoryTheory.Limits.preservesLimitsOfShapeOfNatIso

deleted theorem CategoryTheory.Limits.preservesLimitsOfShapeOfReflectsOfPreserves

deleted theorem CategoryTheory.Limits.preservesLimitsOfSizeOfUnivLE

deleted theorem CategoryTheory.Limits.preservesSmallestColimitsOfPreservesColimits

deleted theorem CategoryTheory.Limits.preservesSmallestLimitsOfPreservesLimits

deleted theorem CategoryTheory.Limits.reflectsColimitOfIsoDiagram

deleted theorem CategoryTheory.Limits.reflectsColimitOfNatIso

deleted theorem CategoryTheory.Limits.reflectsColimitOfReflectsIsomorphisms

deleted theorem CategoryTheory.Limits.reflectsColimitsOfNatIso

deleted theorem CategoryTheory.Limits.reflectsColimitsOfReflectsIsomorphisms

deleted theorem CategoryTheory.Limits.reflectsColimitsOfShapeOfEquiv

deleted theorem CategoryTheory.Limits.reflectsColimitsOfShapeOfNatIso

deleted theorem CategoryTheory.Limits.reflectsColimitsOfShapeOfReflectsIsomorphisms

deleted theorem CategoryTheory.Limits.reflectsColimitsOfSizeOfUnivLE

deleted theorem CategoryTheory.Limits.reflectsColimitsOfSizeShrink

deleted theorem CategoryTheory.Limits.reflectsLimitOfIsoDiagram

deleted theorem CategoryTheory.Limits.reflectsLimitOfNatIso

deleted theorem CategoryTheory.Limits.reflectsLimitOfReflectsIsomorphisms

deleted theorem CategoryTheory.Limits.reflectsLimitsOfNatIso

deleted theorem CategoryTheory.Limits.reflectsLimitsOfReflectsIsomorphisms

deleted theorem CategoryTheory.Limits.reflectsLimitsOfShapeOfEquiv

deleted theorem CategoryTheory.Limits.reflectsLimitsOfShapeOfNatIso

deleted theorem CategoryTheory.Limits.reflectsLimitsOfShapeOfReflectsIsomorphisms

deleted theorem CategoryTheory.Limits.reflectsLimitsOfSizeOfUnivLE

deleted theorem CategoryTheory.Limits.reflectsLimitsOfSizeShrink

deleted theorem CategoryTheory.Limits.reflectsSmallestColimitsOfReflectsColimits

deleted theorem CategoryTheory.Limits.reflectsSmallestLimitsOfReflectsLimits

Modified Mathlib/CategoryTheory/Limits/Preserves/Opposites.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Countable.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Basic.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean

Modified Mathlib/CategoryTheory/Monoidal/Bimon_.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

Modified Mathlib/CategoryTheory/Products/Basic.lean

Modified Mathlib/CategoryTheory/Shift/CommShift.lean

Modified Mathlib/CategoryTheory/Sites/Adjunction.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/LocallySurjective.lean

Modified Mathlib/CategoryTheory/Sites/Continuous.lean

Modified Mathlib/CategoryTheory/Sites/CoversTop.lean

Modified Mathlib/CategoryTheory/Sites/LocallySurjective.lean

Modified Mathlib/CategoryTheory/Sites/Sheaf.lean

Modified Mathlib/CategoryTheory/Sites/Types.lean

Modified Mathlib/Combinatorics/Additive/RuzsaCovering.lean

Modified Mathlib/Combinatorics/Enumerative/Partition.lean

Modified Mathlib/Condensed/Discrete/Characterization.lean

Modified Mathlib/Data/Complex/Basic.lean

Modified Mathlib/Data/ENNReal/Operations.lean

Modified Mathlib/Data/EReal/Operations.lean

Modified Mathlib/Data/Finmap.lean

Modified Mathlib/Data/Finset/Image.lean

Modified Mathlib/Data/Finset/Insert.lean

Modified Mathlib/Data/Finset/NAry.lean

Modified Mathlib/Data/Fintype/Card.lean

Modified Mathlib/Data/Fintype/EquivFin.lean

Modified Mathlib/Data/Fintype/Perm.lean

Modified Mathlib/Data/Fintype/Units.lean

Modified Mathlib/Data/Int/ModEq.lean

Modified Mathlib/Data/List/AList.lean

Modified Mathlib/Data/List/Enum.lean

Modified Mathlib/Data/List/Lemmas.lean

Modified Mathlib/Data/List/Lex.lean

Modified Mathlib/Data/List/MinMax.lean

Modified Mathlib/Data/List/OfFn.lean

deleted theorem List.last_ofFn

deleted theorem List.last_ofFn_succ

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

deleted theorem List.cons_subperm_of_mem

Modified Mathlib/Data/List/ToFinsupp.lean

Modified Mathlib/Data/Matrix/ColumnRowPartitioned.lean

Modified Mathlib/Data/Matrix/Mul.lean

Modified Mathlib/Data/Matrix/Notation.lean

Modified Mathlib/Data/Matrix/RowCol.lean

Modified Mathlib/Data/Matroid/Basic.lean

Modified Mathlib/Data/Multiset/UnionInter.lean

Modified Mathlib/Data/NNReal/Defs.lean

deleted theorem NNReal.div_le_div_left_of_le

Modified Mathlib/Data/Nat/Bitwise.lean

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

deleted theorem Nat.cast_eq_ofNat

Modified Mathlib/Data/Nat/Factorization/Basic.lean

Modified Mathlib/Data/Nat/Init.lean

deleted theorem Nat.div_lt_iff_lt_mul'

deleted theorem Nat.le_div_iff_mul_le'

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

Modified Mathlib/Data/PFunctor/Univariate/M.lean

Modified Mathlib/Data/Quot.lean

Modified Mathlib/Data/Real/ENatENNReal.lean

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/Data/Set/Image.lean

Modified Mathlib/Data/Set/Lattice.lean

Modified Mathlib/Data/Set/NAry.lean

Modified Mathlib/Data/Vector/Basic.lean

Modified Mathlib/Data/W/Cardinal.lean

Modified Mathlib/Data/ZMod/Units.lean

Modified Mathlib/Dynamics/Minimal.lean

Modified Mathlib/Dynamics/Newton.lean

Modified Mathlib/FieldTheory/Finite/GaloisField.lean

Modified Mathlib/FieldTheory/Fixed.lean

Modified Mathlib/FieldTheory/IntermediateField/Basic.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

Modified Mathlib/FieldTheory/IsSepClosed.lean

Modified Mathlib/FieldTheory/RatFunc/Defs.lean

Modified Mathlib/Geometry/Manifold/Algebra/LieGroup.lean

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

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

Modified Mathlib/Geometry/Manifold/DerivationBundle.lean

Modified Mathlib/Geometry/Manifold/Instances/Real.lean

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

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

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

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

Modified Mathlib/Geometry/Manifold/Metrizable.lean

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

Modified Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean

Modified Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean

Modified Mathlib/GroupTheory/Complement.lean

deleted theorem Subgroup.card_left_transversal

deleted theorem Subgroup.card_right_transversal

deleted theorem Subgroup.exists_left_transversal

deleted theorem Subgroup.exists_right_transversal

deleted def Subgroup.leftTransversals

deleted theorem Subgroup.mem_leftTransversals_iff_bijective

deleted theorem Subgroup.mem_leftTransversals_iff_existsUnique_inv_mul_mem

deleted theorem Subgroup.mem_leftTransversals_iff_existsUnique_quotient_mk''_eq

deleted theorem Subgroup.mem_rightTransversals_iff_bijective

deleted theorem Subgroup.mem_rightTransversals_iff_existsUnique_mul_inv_mem

deleted theorem Subgroup.mem_rightTransversals_iff_existsUnique_quotient_mk''_eq

deleted theorem Subgroup.range_mem_leftTransversals

deleted theorem Subgroup.range_mem_rightTransversals

deleted def Subgroup.rightTransversals

Modified Mathlib/GroupTheory/CosetCover.lean

Modified Mathlib/GroupTheory/GroupAction/Blocks.lean

Modified Mathlib/GroupTheory/Index.lean

Modified Mathlib/GroupTheory/Nilpotent.lean

Modified Mathlib/GroupTheory/NoncommPiCoprod.lean

Modified Mathlib/GroupTheory/Perm/Fin.lean

Modified Mathlib/GroupTheory/Schreier.lean

Modified Mathlib/GroupTheory/SchurZassenhaus.lean

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

Modified Mathlib/GroupTheory/Sylow.lean

Modified Mathlib/GroupTheory/Transfer.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

Modified Mathlib/LinearAlgebra/Alternating/Basic.lean

Modified Mathlib/LinearAlgebra/DFinsupp.lean

Modified Mathlib/LinearAlgebra/Dimension/Basic.lean

Modified Mathlib/LinearAlgebra/Dimension/Finite.lean

Modified Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean

Modified Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

deleted theorem Module.End.disjoint_iSup_genEigenspace

deleted theorem Module.End.genEigenrange_def

deleted theorem Module.End.genEigenspace_def

deleted theorem Module.End.iSup_genEigenspace_inf_le_add

deleted theorem Module.End.iSup_genEigenspace_le_smul

deleted theorem Module.End.independent_iSup_genEigenspace

deleted theorem Module.End.injOn_iSup_genEigenspace

deleted theorem Module.End.isNilpotent_restrict_iSup_sub_algebraMap

deleted theorem Module.End.map_add_of_iInf_iSup_genEigenspace_ne_bot_of_commute

deleted theorem Module.End.map_smul_of_iInf_iSup_genEigenspace_ne_bot

deleted theorem Module.End.mapsTo_iSup_genEigenspace_of_comm

deleted theorem Module.End.maxGenEigenspace_def

Modified Mathlib/LinearAlgebra/FreeModule/Finite/Matrix.lean

Modified Mathlib/LinearAlgebra/FreeProduct/Basic.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

Modified Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean

Modified Mathlib/LinearAlgebra/Matrix/DotProduct.lean

Modified Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean

Modified Mathlib/LinearAlgebra/Matrix/Permanent.lean

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

Modified Mathlib/LinearAlgebra/PiTensorProduct.lean

Modified Mathlib/LinearAlgebra/Projectivization/Independence.lean

Modified Mathlib/Logic/Embedding/Basic.lean

Modified Mathlib/Logic/Equiv/Defs.lean

Modified Mathlib/Logic/ExistsUnique.lean

Modified Mathlib/Logic/Function/Basic.lean

Modified Mathlib/Logic/Unique.lean

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

Modified Mathlib/MeasureTheory/Covering/Differentiation.lean

Modified Mathlib/MeasureTheory/Covering/Vitali.lean

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

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Indicator.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean

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

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

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Defs.lean

Modified Mathlib/MeasureTheory/Function/LpSpace/Indicator.lean

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/Basic.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Norm.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Prod.lean

Modified Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean

Modified Mathlib/MeasureTheory/Measure/Count.lean

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

Modified Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

Modified Mathlib/MeasureTheory/Measure/Map.lean

Modified Mathlib/MeasureTheory/Measure/Regular.lean

Modified Mathlib/ModelTheory/PartialEquiv.lean

Modified Mathlib/NumberTheory/DirichletCharacter/Basic.lean

Modified Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean

Modified Mathlib/NumberTheory/Fermat.lean

Modified Mathlib/NumberTheory/Multiplicity.lean

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

Modified Mathlib/NumberTheory/NumberField/Completion.lean

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

Modified Mathlib/NumberTheory/Padics/PadicIntegers.lean

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean

Modified Mathlib/NumberTheory/Padics/RingHoms.lean

Modified Mathlib/NumberTheory/RamificationInertia/Basic.lean

Modified Mathlib/Order/Antisymmetrization.lean

Modified Mathlib/Order/Basic.lean

Modified Mathlib/Order/CompactlyGenerated/Basic.lean

Modified Mathlib/Order/CompleteLattice/Basic.lean

deleted theorem iInf_le'

deleted theorem le_iSup'

Modified Mathlib/Order/Disjoint.lean

Modified Mathlib/Order/Filter/Defs.lean

Modified Mathlib/Order/Ideal.lean

Modified Mathlib/Order/InitialSeg.lean

Modified Mathlib/Order/KrullDimension.lean

Modified Mathlib/Order/Lattice.lean

deleted theorem inf_eq_min

deleted theorem sup_eq_max

Modified Mathlib/Order/Monotone/Basic.lean

Modified Mathlib/Order/Notation.lean

Modified Mathlib/Order/Preorder/Chain.lean

Modified Mathlib/Order/RelIso/Basic.lean

Modified Mathlib/Order/SupIndep.lean

Modified Mathlib/Probability/BorelCantelli.lean

Modified Mathlib/Probability/Density.lean

Modified Mathlib/Probability/Independence/ZeroOne.lean

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

Modified Mathlib/Probability/Kernel/CondDistrib.lean

Modified Mathlib/Probability/Kernel/Condexp.lean

Modified Mathlib/Probability/Kernel/Proper.lean

Modified Mathlib/Probability/Martingale/Basic.lean

Modified Mathlib/Probability/Martingale/Convergence.lean

Modified Mathlib/Probability/Martingale/OptionalSampling.lean

Modified Mathlib/Probability/Moments/Variance.lean

Modified Mathlib/Probability/Process/Stopping.lean

Modified Mathlib/RingTheory/Algebraic/Basic.lean

Modified Mathlib/RingTheory/Algebraic/Cardinality.lean

Modified Mathlib/RingTheory/Algebraic/Defs.lean

Modified Mathlib/RingTheory/Algebraic/Integral.lean

Modified Mathlib/RingTheory/Algebraic/Pi.lean

Modified Mathlib/RingTheory/Artinian/Module.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

Modified Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean

Modified Mathlib/RingTheory/Filtration.lean

Modified Mathlib/RingTheory/Finiteness/Cardinality.lean

Modified Mathlib/RingTheory/Finiteness/Ideal.lean

Modified Mathlib/RingTheory/Flat/Basic.lean

Modified Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean

Modified Mathlib/RingTheory/Flat/Stability.lean

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

Modified Mathlib/RingTheory/Ideal/Cotangent.lean

Modified Mathlib/RingTheory/Ideal/Maps.lean

Modified Mathlib/RingTheory/Ideal/Over.lean

Modified Mathlib/RingTheory/Idempotents.lean

Modified Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean

Modified Mathlib/RingTheory/Jacobson/Ring.lean

Modified Mathlib/RingTheory/KrullDimension/Zero.lean

deleted theorem IsLocalization.AtPrime.prime_unique_of_minimal

Modified Mathlib/RingTheory/LocalRing/Basic.lean

Modified Mathlib/RingTheory/LocalRing/Defs.lean

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

Modified Mathlib/RingTheory/LocalRing/MaximalIdeal/Defs.lean

Modified Mathlib/RingTheory/LocalRing/Module.lean

Modified Mathlib/RingTheory/LocalRing/Quotient.lean

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

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

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

Modified Mathlib/RingTheory/Localization/AtPrime/Basic.lean

Modified Mathlib/RingTheory/Localization/Away/Basic.lean

Modified Mathlib/RingTheory/Localization/BaseChange.lean

Modified Mathlib/RingTheory/Localization/Cardinality.lean

Modified Mathlib/RingTheory/Localization/FractionRing.lean

Modified Mathlib/RingTheory/Multiplicity.lean

Modified Mathlib/RingTheory/MvPolynomial.lean

Modified Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

Modified Mathlib/RingTheory/Noetherian/Basic.lean

Modified Mathlib/RingTheory/NonUnitalSubring/Basic.lean

Modified Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Chebyshev.lean

Modified Mathlib/RingTheory/Polynomial/HilbertPoly.lean

Modified Mathlib/RingTheory/Polynomial/IntegralNormalization.lean

Modified Mathlib/RingTheory/Polynomial/Wronskian.lean

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

Modified Mathlib/RingTheory/PowerSeries/Order.lean

Modified Mathlib/RingTheory/PrincipalIdealDomain.lean

Modified Mathlib/RingTheory/Regular/RegularSequence.lean

Modified Mathlib/RingTheory/SimpleModule/Basic.lean

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

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

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean

Modified Mathlib/RingTheory/Unramified/Field.lean

Modified Mathlib/RingTheory/Valuation/Basic.lean

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

deleted theorem Cardinal.principal_add_aleph

Modified Mathlib/SetTheory/Cardinal/Subfield.lean

Modified Mathlib/SetTheory/Cardinal/ToNat.lean

Modified Mathlib/SetTheory/Game/Nim.lean

Modified Mathlib/SetTheory/Game/Ordinal.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

Modified Mathlib/SetTheory/Ordinal/Family.lean

Modified Mathlib/SetTheory/Ordinal/Topology.lean

Modified Mathlib/SetTheory/PGame/Algebra.lean

deleted theorem SetTheory.PGame.moveLeft_neg_symm'

deleted theorem SetTheory.PGame.moveLeft_neg_symm

deleted theorem SetTheory.PGame.moveRight_neg_symm'

deleted theorem SetTheory.PGame.moveRight_neg_symm

Modified Mathlib/Tactic/DefEqTransformations.lean

Modified Mathlib/Tactic/Linter/OldObtain.lean

deleted def Mathlib.Linter.Style.is_obtain_without_proof

Modified Mathlib/Tactic/Linter/Style.lean

deleted def Mathlib.Linter.Style.setOption.is_set_option

deleted def Mathlib.Linter.Style.setOption.parse_set_option

Modified Mathlib/Tactic/MoveAdd.lean

Modified Mathlib/Topology/AlexandrovDiscrete.lean

Modified Mathlib/Topology/Algebra/Algebra.lean

Modified Mathlib/Topology/Algebra/ConstMulAction.lean

Modified Mathlib/Topology/Algebra/Constructions.lean

Modified Mathlib/Topology/Algebra/Constructions/DomMulAct.lean

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

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

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

Modified Mathlib/Topology/Algebra/GroupWithZero.lean

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

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

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

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

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

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

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

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

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

Modified Mathlib/Topology/Algebra/Monoid.lean

Modified Mathlib/Topology/Algebra/MulAction.lean

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

Modified Mathlib/Topology/Algebra/Ring/Ideal.lean

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

Modified Mathlib/Topology/Algebra/StarSubalgebra.lean

Modified Mathlib/Topology/Algebra/UniformRing.lean

Modified Mathlib/Topology/Bases.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling/Induction.lean

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

Modified Mathlib/Topology/Category/TopCat/Limits/Basic.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Products.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean

Modified Mathlib/Topology/Clopen.lean

Modified Mathlib/Topology/ClopenBox.lean

Modified Mathlib/Topology/CompactOpen.lean

Modified Mathlib/Topology/Compactness/Compact.lean

Modified Mathlib/Topology/Compactness/Lindelof.lean

Modified Mathlib/Topology/Compactness/LocallyCompact.lean

Modified Mathlib/Topology/Compactness/SigmaCompact.lean

Modified Mathlib/Topology/Connected/Basic.lean

Modified Mathlib/Topology/Connected/Clopen.lean

Modified Mathlib/Topology/Connected/LocallyConnected.lean

Modified Mathlib/Topology/Connected/PathConnected.lean

Modified Mathlib/Topology/Connected/TotallyDisconnected.lean

Modified Mathlib/Topology/Constructions.lean

Modified Mathlib/Topology/Constructions/SumProd.lean

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

Modified Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean

Modified Mathlib/Topology/ContinuousMap/Sigma.lean

Modified Mathlib/Topology/ContinuousMap/T0Sierpinski.lean

Modified Mathlib/Topology/ContinuousOn.lean

Modified Mathlib/Topology/Covering.lean

Modified Mathlib/Topology/Defs/Induced.lean

Modified Mathlib/Topology/DenseEmbedding.lean

Modified Mathlib/Topology/DiscreteQuotient.lean

Modified Mathlib/Topology/FiberBundle/Basic.lean

Modified Mathlib/Topology/FiberBundle/Constructions.lean

Modified Mathlib/Topology/FiberBundle/IsHomeomorphicTrivialBundle.lean

Modified Mathlib/Topology/Filter.lean

Modified Mathlib/Topology/GDelta/Basic.lean

Modified Mathlib/Topology/Homeomorph/Defs.lean

Modified Mathlib/Topology/Homeomorph/Lemmas.lean

Modified Mathlib/Topology/Inseparable.lean

Modified Mathlib/Topology/Instances/Discrete.lean

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

Modified Mathlib/Topology/Instances/ENat.lean

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

Modified Mathlib/Topology/Instances/Matrix.lean

Modified Mathlib/Topology/Instances/Rat.lean

Modified Mathlib/Topology/Instances/TrivSqZeroExt.lean

Modified Mathlib/Topology/Irreducible.lean

Modified Mathlib/Topology/LocalAtTarget.lean

Modified Mathlib/Topology/LocallyClosed.lean

Modified Mathlib/Topology/Maps/Basic.lean

Modified Mathlib/Topology/Maps/OpenQuotient.lean

Modified Mathlib/Topology/MetricSpace/Basic.lean

Modified Mathlib/Topology/MetricSpace/Dilation.lean

Modified Mathlib/Topology/MetricSpace/Isometry.lean

Modified Mathlib/Topology/MetricSpace/ProperSpace.lean

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

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

Modified Mathlib/Topology/Metrizable/Basic.lean

Modified Mathlib/Topology/Metrizable/Urysohn.lean

Modified Mathlib/Topology/NoetherianSpace.lean

Modified Mathlib/Topology/Order/Basic.lean

Modified Mathlib/Topology/Order/DenselyOrdered.lean

deleted theorem nhdsWithin_Iio_self_neBot

deleted theorem nhdsWithin_Ioi_self_neBot

Modified Mathlib/Topology/Order/LeftRight.lean

deleted theorem nhdsWithin_Ici_self_neBot

deleted theorem nhdsWithin_Iic_self_neBot

Modified Mathlib/Topology/Order/LeftRightNhds.lean

Modified Mathlib/Topology/Order/LowerUpperTopology.lean

Modified Mathlib/Topology/Order/Monotone.lean

Modified Mathlib/Topology/Order/OrderClosed.lean

Modified Mathlib/Topology/Order/ProjIcc.lean

Modified Mathlib/Topology/Order/T5.lean

Modified Mathlib/Topology/QuasiSeparated.lean

Modified Mathlib/Topology/SeparatedMap.lean

Modified Mathlib/Topology/Separation/Basic.lean

Modified Mathlib/Topology/Separation/Hausdorff.lean

Modified Mathlib/Topology/Separation/Profinite.lean

Modified Mathlib/Topology/Separation/Regular.lean

Modified Mathlib/Topology/Sequences.lean

Modified Mathlib/Topology/Sheaves/CommRingCat.lean

deleted theorem CommRingCat.presheaf_restrict_restrict

Modified Mathlib/Topology/Sheaves/Stalks.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/UniformEmbedding.lean

Modified docs/overview.yaml