Commit 2025-04-23 11:03 8514782c

View on Github →

chore: delete >6 month old deprecations (2024-10 11-21) (#24271) The first commit was done automatically using #21271's method, with the regex

@\[deprecated.*\(since := "2024-10-([01].|2[01])"\)\][\s\n]?(protected )?alias [_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟'.₀₁₂₃₄₅₆₇₈₉]* :=[\s\n]+[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟'.₀₁₂₃₄₅₆₇₈₉]*\n\n?

The remaining commits are manual removals of empty sections and missed deprecations (2024-10-([01].|2[01])).

Estimated changes

deleted theorem Cardinal.aleph'_isNormal
deleted theorem Cardinal.aleph'_le
deleted theorem Cardinal.aleph'_limit
deleted theorem Cardinal.aleph'_lt
deleted theorem Cardinal.aleph'_max
deleted theorem Cardinal.aleph'_nat
deleted theorem Cardinal.aleph'_omega0
deleted theorem Cardinal.aleph'_pos
deleted theorem Cardinal.aleph'_succ
deleted theorem Cardinal.aleph'_zero
deleted theorem Cardinal.aleph0_le_aleph'
deleted theorem Cardinal.aleph_eq_aleph'
deleted theorem Cardinal.aleph_isNormal
deleted theorem Cardinal.beth_normal
deleted theorem Cardinal.exists_aleph
deleted theorem Cardinal.lift_aleph'