Commit 2024-09-18 21:33 617f330d

View on Github →

feat(SetTheory/Ordinal/Basic): added ord_zero_iff lemma (#16912) Prove ord_zero_iff.

Estimated changes

added theorem Cardinal.ord_eq_one
added theorem Cardinal.ord_eq_zero
added theorem Cardinal.ord_inj