Commit 2025-11-28 15:51 ceaf1271

View on Github →

refactor(SetTheory/Ordinal): use generic order lemmas (#31883) ... and deprecate the custom Ordinal ones

Estimated changes

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

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

Modified Mathlib/SetTheory/Game/Birthday.lean

Modified Mathlib/SetTheory/Game/Nim.lean

Modified Mathlib/SetTheory/Game/Ordinal.lean

Modified Mathlib/SetTheory/Nimber/Basic.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

modified theorem Ordinal.div_le_of_le_mul

modified theorem Ordinal.sub_le_self

modified theorem Ordinal.zero_div

modified theorem Ordinal.zero_sub

Modified Mathlib/SetTheory/Ordinal/Basic.lean

deleted theorem Ordinal.eq_zero_or_pos

deleted theorem Ordinal.le_add_left

deleted theorem Ordinal.le_add_right

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

Modified Mathlib/SetTheory/Ordinal/Family.lean

Modified Mathlib/SetTheory/Ordinal/FixedPoint.lean

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean

deleted theorem NatOrdinal.zero_le

modified theorem Ordinal.le_nadd_self

modified theorem Ordinal.le_self_nadd

Modified Mathlib/SetTheory/Ordinal/Notation.lean

Modified Mathlib/SetTheory/Ordinal/Principal.lean

Modified Mathlib/SetTheory/Ordinal/Topology.lean

Modified Mathlib/SetTheory/Ordinal/Veblen.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling/Induction.lean