Commit 2024-11-13 20:03 043fac94

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

Modified Mathlib/Algebra/Group/Nat.lean

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

Modified Mathlib/Algebra/Order/Group/Unbundled/Abs.lean

Modified Mathlib/Analysis/Asymptotics/Asymptotics.lean

Modified Mathlib/Analysis/LocallyConvex/Bounded.lean

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

Modified Mathlib/Analysis/SpecialFunctions/Exp.lean

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

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

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

Modified Mathlib/Analysis/SpecificLimits/Basic.lean

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

Modified Mathlib/Analysis/SpecificLimits/RCLike.lean

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/Data/Finset/Image.lean

deleted theorem Finset.Nonempty.image_iff

Modified Mathlib/Data/Fintype/Order.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/Set/Function.lean

deleted theorem Set.maps_range_to

Modified Mathlib/Data/Set/Image.lean

Modified Mathlib/FieldTheory/Adjoin.lean

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

Modified Mathlib/GroupTheory/Exponent.lean

deleted theorem Monoid.exponentExists_iff_ne_zero

deleted theorem Monoid.exponent_dvd_of_forall_orderOf_dvd

Modified Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean

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

Modified Mathlib/Logic/Equiv/Set.lean

Modified Mathlib/Logic/Function/Defs.lean

deleted def Function.app

deleted def Function.combine

deleted def Function.compLeft

deleted def Function.compRight

Modified Mathlib/MeasureTheory/Group/Measure.lean

deleted theorem IsCompact.closure_subset_of_measurableSet_of_group

deleted theorem IsCompact.measure_closure_eq_of_group

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

deleted theorem MeasureTheory.measure_iUnion_null_iff'

Modified Mathlib/MeasureTheory/Measure/Regular.lean

Modified Mathlib/MeasureTheory/OuterMeasure/Basic.lean

deleted theorem MeasureTheory.OuterMeasure.iUnion_null_iff'

Modified Mathlib/RingTheory/Ideal/Operations.lean

deleted theorem Ideal.prod_eq_bot

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

deleted theorem exists_isCompact_isClosed_nhds_one

deleted theorem exists_isCompact_isClosed_subset_isCompact_nhds_one

deleted theorem instLocallyCompactSpaceOfWeaklyOfGroup

deleted theorem local_isCompact_isClosed_nhds_of_group

Modified Mathlib/Topology/Basic.lean

deleted theorem eventuallyEq_zero_nhds

Modified Mathlib/Topology/Bornology/Absorbs.lean

Modified Mathlib/Topology/CompactOpen.lean

deleted theorem ContinuousMap.continuous.comp'

Modified Mathlib/Topology/Compactness/Compact.lean

Modified Mathlib/Topology/MetricSpace/ProperSpace.lean

Modified Mathlib/Topology/Separation/Basic.lean

deleted theorem T4Space.of_compactSpace_t2Space

Modified Mathlib/Topology/TietzeExtension.lean

Modified Mathlib/Topology/Ultrafilter.lean