Commit 2026-07-15 16:59 5ad5d522

chore: delete deprecated declarations to the end of 2025 (#41178) The automated commits were made by running

#clear_deprecations "2025-11-01" "2025-12-31" really

(I had to do this in multiple sessions because VS Code kept running out of memory.)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Basic.lean

deleted theorem Algebra.algebraMap_ofSubring_apply

deleted theorem Algebra.coe_algebraMap_ofSubring

Modified Mathlib/Algebra/Algebra/Bilinear.lean

Modified Mathlib/Algebra/Algebra/Defs.lean

deleted theorem Algebra.id.smul_eq_mul

Modified Mathlib/Algebra/Algebra/Equiv.lean

Modified Mathlib/Algebra/BigOperators/Finsupp/Basic.lean

deleted theorem Finsupp.sum_zero

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

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

Modified Mathlib/Algebra/DirectSum/Module.lean

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

deleted theorem Set.op_smul_inter_ne_empty_iff

deleted theorem Set.smul_inter_ne_empty_iff'

deleted theorem Set.smul_inter_ne_empty_iff

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

Modified Mathlib/Algebra/Group/Indicator.lean

Modified Mathlib/Algebra/Group/Irreducible/Indecomposable.lean

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

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

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

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

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

Modified Mathlib/Algebra/Order/AddGroupWithTop.lean

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

Deleted Mathlib/Algebra/Order/Field/Defs.lean

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

deleted theorem Int.add_one_le_ceil_iff

deleted theorem Int.floor_le_sub_one_iff

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

deleted theorem ofAdd_bot

deleted theorem ofAdd_toDual_eq_zero_iff

deleted theorem ofDual_toAdd_eq_top_iff

Modified Mathlib/Algebra/Order/IsBotOne.lean

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

deleted theorem ArchimedeanClass.ball_antitone

deleted theorem ArchimedeanClass.ball_le_closedBall

deleted theorem ArchimedeanClass.ball_top

deleted theorem ArchimedeanClass.closedBall_top

deleted theorem ArchimedeanClass.mem_ball_iff

deleted theorem ArchimedeanClass.mem_closedBall_iff

deleted def ArchimedeanClass.submodule

deleted theorem ArchimedeanClass.toAddSubgroup_ball

deleted theorem ArchimedeanClass.toAddSubgroup_closedBall

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

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

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

Modified Mathlib/Algebra/Polynomial/Bivariate.lean

Modified Mathlib/Algebra/Polynomial/Derivative.lean

Modified Mathlib/Algebra/Polynomial/Expand.lean

Modified Mathlib/Algebra/Polynomial/Roots.lean

Modified Mathlib/Algebra/Polynomial/Splits.lean

deleted theorem Polynomial.rootOfSplits'_eq_rootOfSplits

deleted theorem Polynomial.splits_id_iff_splits

deleted theorem Polynomial.splits_map_iff

deleted theorem Polynomial.splits_of_map_eq_C

deleted theorem Polynomial.splits_of_splits_gcd_left

deleted theorem Polynomial.splits_of_splits_gcd_right

Modified Mathlib/Algebra/QuadraticAlgebra/Basic.lean

Modified Mathlib/Algebra/QuadraticAlgebra/Defs.lean

Modified Mathlib/Algebra/Quotient.lean

Modified Mathlib/Algebra/Ring/Equiv.lean

Modified Mathlib/Algebra/Star/LinearMap.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean

Modified Mathlib/Analysis/Analytic/Binomial.lean

Modified Mathlib/Analysis/Analytic/OfScalars.lean

Modified Mathlib/Analysis/CStarAlgebra/Unitary/Connected.lean

Modified Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean

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

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

Modified Mathlib/Analysis/Complex/Basic.lean

Modified Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction.lean

Modified Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Basic.lean

Modified Mathlib/Analysis/Complex/ValueDistribution/Proximity/Basic.lean

Modified Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace/Deriv.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace/Fourier.lean

Modified Mathlib/Analysis/Distribution/TemperedDistribution.lean

Modified Mathlib/Analysis/Distribution/TestFunction.lean

Modified Mathlib/Analysis/Fourier/FourierTransform.lean

Modified Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

Modified Mathlib/Analysis/Fourier/Inversion.lean

Modified Mathlib/Analysis/Fourier/LpSpace.lean

Modified Mathlib/Analysis/Fourier/PoissonSummation.lean

Modified Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

Modified Mathlib/Analysis/InnerProductSpace/Laplacian.lean

Modified Mathlib/Analysis/InnerProductSpace/Orthogonal.lean

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection/Submodule.lean

Modified Mathlib/Analysis/InnerProductSpace/Symmetric.lean

Modified Mathlib/Analysis/Matrix/Order.lean

Modified Mathlib/Analysis/MellinInversion.lean

Modified Mathlib/Analysis/Meromorphic/Basic.lean

deleted theorem MeromorphicAt.fun_deriv

deleted theorem MeromorphicAt.fun_iterated_deriv

deleted theorem MeromorphicOn.fun_deriv

deleted theorem MeromorphicOn.fun_iterated_deriv

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

deleted theorem NormedField.tendsto_norm_zpow_nhdsNE_zero_atTop

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

deleted theorem AbsoluteValue.Completion.extensionEmbedding_dist_eq_of_comp

deleted theorem AbsoluteValue.Completion.extensionEmbedding_of_comp_coe

deleted theorem AbsoluteValue.Completion.isClosedEmbedding_extensionEmbedding_of_comp

deleted theorem AbsoluteValue.Completion.isometry_extensionEmbedding_of_comp

deleted theorem WithAbs.isUniformInducing_of_comp

deleted theorem WithAbs.isometry_of_comp

deleted theorem WithAbs.pseudoMetricSpace_induced_of_comp

deleted theorem WithAbs.uniformSpace_comap_eq_of_comp

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

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

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

deleted theorem LinearIsometry.isComplete_image_iff'

Modified Mathlib/Analysis/Polynomial/MahlerMeasure.lean

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

Modified Mathlib/CategoryTheory/Abelian/Basic.lean

Modified Mathlib/CategoryTheory/Abelian/SerreClass/Bousfield.lean

Modified Mathlib/CategoryTheory/EffectiveEpi/Basic.lean

Modified Mathlib/CategoryTheory/Functor/KanExtension/DenseAt.lean

Modified Mathlib/CategoryTheory/Groupoid.lean

deleted def CategoryTheory.Groupoid.invFunctor

Modified Mathlib/CategoryTheory/Limits/ExactFunctor.lean

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

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

deleted theorem CategoryTheory.strongEpi_of_regularEpi

Modified Mathlib/CategoryTheory/Localization/Bousfield.lean

Modified Mathlib/CategoryTheory/Localization/DerivabilityStructure/PointwiseRightDerived.lean

Modified Mathlib/CategoryTheory/Localization/Opposite.lean

Modified Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/Grp.lean

Modified Mathlib/CategoryTheory/Monoidal/Closed/Cartesian.lean

Modified Mathlib/CategoryTheory/Monoidal/CommGrp_.lean

Modified Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean

Modified Mathlib/CategoryTheory/Monoidal/Grp.lean

Modified Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.δ_eq

deleted theorem CategoryTheory.monoidalOfHasFiniteProducts.η_eq

Modified Mathlib/CategoryTheory/Monoidal/Subcategory.lean

Modified Mathlib/CategoryTheory/ObjectProperty/FullSubcategory.lean

Modified Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean

Modified Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean

Modified Mathlib/CategoryTheory/Quotient.lean

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

Modified Mathlib/CategoryTheory/Sites/Localization.lean

Modified Mathlib/CategoryTheory/Sites/Subcanonical.lean

Modified Mathlib/CategoryTheory/Sites/Subsheaf.lean

Modified Mathlib/CategoryTheory/Skeletal.lean

Modified Mathlib/CategoryTheory/Subfunctor/Basic.lean

Modified Mathlib/CategoryTheory/Subfunctor/Equalizer.lean

Modified Mathlib/CategoryTheory/Subfunctor/Finite.lean

Modified Mathlib/CategoryTheory/Subfunctor/Image.lean

Modified Mathlib/CategoryTheory/Subfunctor/OfSection.lean

Modified Mathlib/CategoryTheory/Subfunctor/Sieves.lean

Modified Mathlib/CategoryTheory/Subfunctor/Subobject.lean

Modified Mathlib/CategoryTheory/Subobject/Basic.lean

Modified Mathlib/CategoryTheory/Subobject/Classifier/Defs.lean

Modified Mathlib/CategoryTheory/Subobject/MonoOver.lean

Modified Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean

Modified Mathlib/CategoryTheory/Yoneda.lean

deleted def CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight

deleted def CategoryTheory.Functor.FullyFaithful.homNatIsoMaxRight

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Metric.lean

deleted theorem SimpleGraph.Connected.diff_dist_adj

Modified Mathlib/Combinatorics/SimpleGraph/Walk/Traversal.lean

deleted theorem SimpleGraph.Walk.getLast_darts_snd

deleted theorem SimpleGraph.Walk.head_darts_fst

Modified Mathlib/Computability/NFA.lean

deleted theorem NFA.evalFrom_append_singleton

deleted theorem NFA.evalFrom_biUnion

Modified Mathlib/Data/DFinsupp/Lex.lean

Modified Mathlib/Data/ENat/Basic.lean

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/Data/Finset/NoncommProd.lean

Modified Mathlib/Data/Finset/Sort.lean

Modified Mathlib/Data/Finsupp/Basic.lean

Modified Mathlib/Data/Finsupp/Interval.lean

Modified Mathlib/Data/Finsupp/Lex.lean

Modified Mathlib/Data/Finsupp/Weight.lean

Modified Mathlib/Data/Fintype/Card.lean

Modified Mathlib/Data/Int/ConditionallyCompleteOrder.lean

Modified Mathlib/Data/Int/Fib/Basic.lean

deleted theorem Int.fib_gcd

Modified Mathlib/Data/List/Chain.lean

deleted theorem List.isChain_cons_iff_get

deleted theorem List.isChain_iff_get

Modified Mathlib/Data/List/Cycle.lean

Modified Mathlib/Data/List/GetD.lean

Modified Mathlib/Data/List/Sort.lean

deleted theorem List.sorted_le_range'

deleted theorem List.sorted_le_range

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

deleted theorem Nat.succ_mul_choose_eq

Modified Mathlib/Data/Rat/Lemmas.lean

deleted theorem Rat.den_mk

deleted theorem Rat.num_mk

Modified Mathlib/Data/Rel/Cover.lean

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/Data/Sym/Sym2.lean

deleted theorem Sym2.diagSet_compl_eq_setOf_not_isDiag

deleted theorem Sym2.irreflexive_iff_fromRel_subset_diagSet_compl

deleted theorem Sym2.mem_diagSet_iff_isDiag

deleted theorem Sym2.reflexive_iff_diagSet_subset_fromRel

Modified Mathlib/Dynamics/Ergodic/Ergodic.lean

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean

deleted theorem IntermediateField.adjoin_simple_toSubalgebra_of_integral

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

deleted theorem IsAlgClosed.splits_codomain

Modified Mathlib/FieldTheory/IsSepClosed.lean

Modified Mathlib/FieldTheory/Normal/Closure.lean

Modified Mathlib/FieldTheory/SeparableClosure.lean

Modified Mathlib/FieldTheory/SeparableDegree.lean

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

Modified Mathlib/Geometry/Manifold/Immersion.lean

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

Modified Mathlib/Geometry/Manifold/LocalDiffeomorph.lean

Modified Mathlib/Geometry/Manifold/PartitionOfUnity.lean

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

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

Modified Mathlib/Geometry/RingedSpace/SheafedSpace.lean

Modified Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean

deleted theorem pow_gcd_card_eq_one_iff

Modified Mathlib/GroupTheory/Perm/Cycle/Basic.lean

Modified Mathlib/GroupTheory/Perm/Finite.lean

Modified Mathlib/GroupTheory/Perm/MaximalSubgroups.lean

Modified Mathlib/GroupTheory/Perm/Support.lean

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean

deleted theorem LinearMap.mul_eq_one_comm

deleted theorem LinearMap.mul_eq_one_of_mul_eq_one

Modified Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean

deleted theorem Matrix.exists_left_inverse_iff_isUnit

deleted theorem Matrix.exists_right_inverse_iff_isUnit

deleted theorem Matrix.isUnit_of_left_inverse

deleted theorem Matrix.isUnit_of_right_inverse

Modified Mathlib/LinearAlgebra/RootSystem/Basic.lean

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

Modified Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean

Modified Mathlib/LinearAlgebra/Span/Basic.lean

Modified Mathlib/Logic/Relation.lean

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

Modified Mathlib/MeasureTheory/MeasurableSpace/Card.lean

Modified Mathlib/MeasureTheory/Measure/Doubling.lean

Modified Mathlib/MeasureTheory/Measure/Real.lean

Modified Mathlib/MeasureTheory/Measure/RegularityCompacts.lean

Modified Mathlib/MeasureTheory/Measure/Tight.lean

Modified Mathlib/NumberTheory/Bernoulli.lean

Modified Mathlib/NumberTheory/Divisors.lean

Modified Mathlib/NumberTheory/ModularForms/Basic.lean

Modified Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean

deleted theorem EisensteinSeries.linear_isTheta_right

Modified Mathlib/NumberTheory/ModularForms/SlashInvariantForms.lean

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

Modified Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean

Modified Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean

Modified Mathlib/Order/Atoms.lean

deleted theorem CompleteAtomicBooleanAlgebra.exists_mem_le_of_le_sSup_of_isAtom

Modified Mathlib/Order/Basic.lean

deleted theorem le_of_eq_of_le'

deleted theorem le_of_le_of_eq'

deleted theorem lt_of_eq_of_lt'

deleted theorem lt_of_lt_of_eq'

Modified Mathlib/Order/BoundedOrder/Basic.lean

deleted theorem eq_bot_of_minimal

Modified Mathlib/Order/Category/FinPartOrd.lean

Modified Mathlib/Order/Category/NonemptyFinLinOrd.lean

Modified Mathlib/Order/CompleteLattice/MulticoequalizerDiagram.lean

Modified Mathlib/Order/Defs/Unbundled.lean

Modified Mathlib/Order/Interval/Set/Basic.lean

deleted theorem Set.left_mem_Ioc

deleted theorem Set.left_mem_Ioo

deleted theorem Set.right_mem_Ico

deleted theorem Set.right_mem_Ioo

Modified Mathlib/Order/Monotone/Defs.lean

deleted theorem injective_of_le_imp_le

Modified Mathlib/Order/PiLex.lean

Modified Mathlib/Order/RelSeries.lean

deleted theorem RelSeries.toList_getElem_eq_apply

deleted theorem RelSeries.toList_getElem_eq_apply_of_lt_length

Modified Mathlib/Order/SetAccumulate.lean

Modified Mathlib/Order/SuccPred/Basic.lean

deleted theorem Order.pred_lt_of_not_isMin_of_le

Modified Mathlib/Order/SuccPred/Limit.lean

Modified Mathlib/Order/WithBot.lean

deleted theorem WithBot.ofDual_symm_apply

deleted theorem WithBot.toDual_symm_apply

Modified Mathlib/Probability/Moments/Covariance.lean

Modified Mathlib/Probability/Moments/Variance.lean

Modified Mathlib/RepresentationTheory/FDRep.lean

Modified Mathlib/RepresentationTheory/Homological/GroupCohomology/Functoriality.lean

Modified Mathlib/RingTheory/AlgebraTower.lean

Modified Mathlib/RingTheory/DividedPowers/Padic.lean

Modified Mathlib/RingTheory/Etale/Basic.lean

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

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

deleted theorem HahnSeries.coeff_order_ne_zero

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

Modified Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean

Modified Mathlib/RingTheory/Ideal/AssociatedPrime/Localization.lean

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

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

Modified Mathlib/RingTheory/MvPolynomial/Expand.lean

Modified Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

Modified Mathlib/RingTheory/PicardGroup.lean

Modified Mathlib/RingTheory/Polynomial/IntegralNormalization.lean

Modified Mathlib/RingTheory/Polynomial/ScaleRoots.lean

Modified Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean

Modified Mathlib/RingTheory/Smooth/Basic.lean

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

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

deleted theorem PrimeSpectrum.comap_apply

Modified Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean

deleted theorem ValuativeRel.srel_iff

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean

Modified Mathlib/SetTheory/Cardinal/Regular.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

deleted theorem Ordinal.IsNormal.id_le

deleted theorem Ordinal.IsNormal.inj

deleted theorem Ordinal.IsNormal.isSuccLimit

deleted theorem Ordinal.IsNormal.le_apply

deleted theorem Ordinal.IsNormal.le_iff

deleted theorem Ordinal.IsNormal.le_iff_eq

deleted theorem Ordinal.IsNormal.le_set'

deleted theorem Ordinal.IsNormal.le_set

deleted theorem Ordinal.IsNormal.limit_le

deleted theorem Ordinal.IsNormal.limit_lt

deleted theorem Ordinal.IsNormal.lt_iff

deleted theorem Ordinal.IsNormal.monotone

deleted theorem Ordinal.IsNormal.refl

deleted theorem Ordinal.IsNormal.strictMono

deleted theorem Ordinal.IsNormal.trans

deleted def Ordinal.boundedLimitRecOn

deleted theorem Ordinal.boundedLimitRec_limit

deleted theorem Ordinal.boundedLimitRec_succ

deleted theorem Ordinal.boundedLimitRec_zero

deleted theorem Ordinal.isNormal_iff_strictMono_limit

Modified Mathlib/SetTheory/Ordinal/Basic.lean

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

Modified Mathlib/SetTheory/Ordinal/Family.lean

deleted theorem Ordinal.IsNormal.apply_of_isSuccLimit

deleted theorem Ordinal.IsNormal.eq_iff_zero_and_succ

deleted theorem Ordinal.IsNormal.map_iSup

deleted theorem Ordinal.IsNormal.map_iSup_of_bddAbove

deleted theorem Ordinal.IsNormal.map_sSup

deleted theorem Ordinal.IsNormal.map_sSup_of_bddAbove

Modified Mathlib/SetTheory/Ordinal/FixedPoint.lean

Modified Mathlib/SetTheory/Ordinal/FundamentalSequence.lean

Modified Mathlib/SetTheory/Ordinal/Veblen.lean

Modified Mathlib/Tactic/Basic.lean

Modified Mathlib/Topology/Algebra/Algebra.lean

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

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

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

Modified Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean

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

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

deleted theorem LinearMap.ker_toContinuousLinearMap

deleted theorem LinearMap.range_toContinuousLinearMap

Modified Mathlib/Topology/Category/UniformSpace.lean

Modified Mathlib/Topology/Compactification/OnePoint/Basic.lean

deleted theorem OnePoint.range_coe_inter_infty

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

Modified Mathlib/Topology/DiscreteSubset.lean

Modified Mathlib/Topology/Homotopy/Lifting.lean

Modified Mathlib/Topology/IsLocalHomeomorph.lean

Modified Mathlib/Topology/MetricSpace/Closeds.lean

Modified Mathlib/Topology/MetricSpace/PiNat.lean

Modified Mathlib/Topology/NoetherianSpace.lean

deleted theorem TopologicalSpace.NoetherianSpace.exists_open_ne_empty_le_irreducibleComponent

Modified Mathlib/Topology/Semicontinuity/Basic.lean

Modified Mathlib/Topology/Sequences.lean

Modified Mathlib/Topology/Sets/Closeds.lean

Modified Mathlib/Topology/UniformSpace/Closeds.lean

Modified Mathlib/Topology/UniformSpace/DiscreteUniformity.lean