Commit 2022-07-06 21:58 0a89f18f

View on Github →

chore(set_theory/ordinal/basic): clean up ordinal.card API (#15147) We tweak some spacing throughout this section of the file, and golf a few theorems/definitions. Conflicts and is inspired by #15137.

Estimated changes

Modified src/set_theory/ordinal/basic.lean

modified def ordinal.card

modified theorem ordinal.card_type

added theorem ordinal.ne_zero_of_out_nonempty

modified theorem ordinal.type_ne_zero_iff_nonempty