Theorem NatOrdinal.zero_le

Modification history

2025-11-28 15:51
Mathlib/SetTheory/Ordinal/NaturalOps.lean
refactor(SetTheory/Ordinal): use generic order lemmas (#31883) …
Deleted NatOrdinal.zero_leView on Github →
2025-03-14 18:18
Mathlib/SetTheory/Ordinal/NaturalOps.lean
feat: more lemmas on `NatOrdinal` (#22616) …
Added NatOrdinal.zero_leView on Github →