Commit 2025-07-12 04:50 82d33c4d

View on Github →

chore(SetTheory/Ordinal/Basic): golf Cardinal.ord proofs (#27011)

Estimated changes

modified theorem Cardinal.card_le_of_le_ord
modified theorem Cardinal.ord_aleph0
modified theorem Cardinal.ord_le
modified theorem Cardinal.ord_nat