Theorem Cardinal.ord_eq_one

Modification history

2024-09-18 21:33
Mathlib/SetTheory/Ordinal/Basic.lean
feat(SetTheory/Ordinal/Basic): added ord_zero_iff lemma (#16912) …
Added Cardinal.ord_eq_oneView on Github →