Theorem Ordinal.eq_natCast_or_omega0_le

Modification history

2026-04-02 20:16
Mathlib/SetTheory/Ordinal/Arithmetic.lean
feat: lemmas on ordinal `Nat.cast` (#36584) …
Added Ordinal.eq_natCast_or_omega0_leView on Github →