Commit 2026-04-02 20:16 8a88eb73

View on Github →

feat: lemmas on ordinal Nat.cast (#36584) Downstreamed from the CGT repo.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

added theorem Ordinal.eq_natCast_of_le_natCast

added theorem Ordinal.eq_natCast_or_omega0_le

deleted theorem Ordinal.eq_nat_or_omega0_le

added theorem Ordinal.natCast_image_Iio