Commit 2025-03-14 18:18 be8a1700

View on Github →

feat: more lemmas on NatOrdinal (#22616) We port some more results on Ordinal into NatOrdinal. Used within the CGT repo.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean

added theorem NatOrdinal.add_le_iff

modified theorem NatOrdinal.bot_eq_zero

added theorem NatOrdinal.lt_add_iff

added theorem NatOrdinal.lt_mul_iff

added theorem NatOrdinal.lt_one_iff_zero

added theorem NatOrdinal.mul_add_lt

added theorem NatOrdinal.mul_le_iff

added theorem NatOrdinal.nmul_nadd_le

added theorem NatOrdinal.not_lt_zero

deleted theorem NatOrdinal.toOrdinal_cast_nat

modified theorem NatOrdinal.toOrdinal_eq_one

modified theorem NatOrdinal.toOrdinal_eq_zero

added theorem NatOrdinal.toOrdinal_natCast

modified theorem NatOrdinal.toOrdinal_one

modified theorem NatOrdinal.toOrdinal_zero

added theorem NatOrdinal.zero_le

deleted theorem Ordinal.toNatOrdinal_cast_nat

modified theorem Ordinal.toNatOrdinal_eq_one

modified theorem Ordinal.toNatOrdinal_eq_zero

added theorem Ordinal.toNatOrdinal_natCast

modified theorem Ordinal.toNatOrdinal_one

modified theorem Ordinal.toNatOrdinal_symm_eq

modified theorem Ordinal.toNatOrdinal_toOrdinal

modified theorem Ordinal.toNatOrdinal_zero