Commit 2024-10-04 11:14 fafd1f69

View on Github →

chore: Delete declarations deprecated in 2023 (#17193) Some of these are on my way.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Group/Finset.lean

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

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

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

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

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

Modified Mathlib/Data/ENNReal/Basic.lean

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/Data/Finset/Image.lean

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.getElem_reverse_aux₂

deleted theorem List.get_reverse_aux₁

deleted theorem List.get_reverse_aux₂

Modified Mathlib/Data/List/Count.lean

deleted theorem List.count_cons'

Modified Mathlib/Data/Multiset/Basic.lean

Modified Mathlib/Data/Nat/Defs.lean

Modified Mathlib/Data/Set/Card.lean

Modified Mathlib/Data/Set/Function.lean

deleted theorem Set.maps_image_to

deleted theorem Set.maps_univ_to

Modified Mathlib/LinearAlgebra/Dimension/Basic.lean

Modified Mathlib/LinearAlgebra/Dimension/Finite.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean

Modified Mathlib/RingTheory/Noetherian.lean

Modified Mathlib/Topology/Bases.lean

Modified Mathlib/Topology/CompactOpen.lean

Modified Mathlib/Topology/Compactness/LocallyCompact.lean

Modified Mathlib/Topology/Order.lean

Modified Mathlib/Topology/Order/LowerUpperTopology.lean

deleted theorem Topology.IsUpper.continuous_of_Iic