Commit 2024-08-20 08:44 63c2523f

View on Github →

chore: remove >1 year deprecations (#15958) This isn't everything with >1year deprecation ages: unfortunately lots is still actually in use!

Estimated changes

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

Modified Mathlib/Algebra/Module/Defs.lean

deleted theorem two_smul'

Modified Mathlib/Algebra/Ring/Int.lean

deleted theorem Int.not_even_bit1

Modified Mathlib/Analysis/Convex/Gauge.lean

deleted theorem gauge_ball'

Modified Mathlib/Analysis/Normed/Affine/Isometry.lean

Modified Mathlib/Data/List/Sort.lean

deleted theorem List.monotone_iff_ofFn_sorted

Modified Mathlib/SetTheory/Lists.lean

deleted def Lists.Equiv.decidableMeas

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

deleted theorem ContinuousOn.exists_forall_ge'

deleted theorem ContinuousOn.exists_forall_le'

deleted theorem IsCompact.exists_forall_ge

deleted theorem IsCompact.exists_forall_le

deleted theorem IsCompact.exists_isLocalMinOn_mem_subset

Modified Mathlib/Topology/PartialHomeomorph.lean

deleted theorem PartialHomeomorph.eq_of_partialEquiv_eq

Modified docs/overview.yaml