Commit 2026-03-26 11:10 c5512575

View on Github →

feat: generalize Ordinal theorems to SuccAddOrder (#37132) We also protect Cardinal theorems of the same names. Note that Cardinal is not a SuccAddOrder.

Estimated changes

Modified Mathlib/Algebra/Order/SuccPred.lean

added theorem Order.le_one_iff

added theorem Order.le_two_iff

added theorem Order.lt_one_iff

added theorem Order.lt_two_iff

added theorem Order.one_le_iff_ne_zero

Modified Mathlib/Combinatorics/SimpleGraph/Extremal/TuranDensity.lean

Modified Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean

Modified Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean

Modified Mathlib/ModelTheory/Encoding.lean

Modified Mathlib/ModelTheory/Semantics.lean

Modified Mathlib/SetTheory/Cardinal/Arithmetic.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

deleted theorem Cardinal.le_one_iff

deleted theorem Cardinal.lt_one_iff_zero

deleted theorem Cardinal.one_le_iff_ne_zero

deleted theorem Cardinal.one_le_iff_pos

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Cardinal/Divisibility.lean

modified theorem Cardinal.le_of_dvd

Modified Mathlib/SetTheory/Cardinal/ENat.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean

deleted theorem Ordinal.le_one_iff

modified theorem Ordinal.lt_one_iff_zero

deleted theorem Ordinal.one_le_iff_ne_zero

Modified Mathlib/SetTheory/Ordinal/CantorNormalForm.lean

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

Modified Mathlib/SetTheory/Ordinal/Principal.lean

Modified Mathlib/SetTheory/Ordinal/Topology.lean