mathlib3

0a89f18f - chore(set_theory/ordinal/basic): clean up `ordinal.card` API (#15147)

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. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>