Theorem Ordinal.eq_natCast_of_le_natCast

Modification history

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