Commit 2022-02-01 09:01 cbad62c5

feat(set_theory/{ordinal_arithmetic, cardinal_ordinal}): Ordinals aren't a small type (#11756) We substantially golf and extend some results previously in cardinal_ordinal.lean.