mathlib3
cbad62c5 - feat(set_theory/{ordinal_arithmetic, cardinal_ordinal}): Ordinals aren't a small type (#11756)

Commit

4 years ago

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`.

Author

vihdzp

Parents

30dcd70e

mathlib3 cbad62c5 - feat(set_theory/{ordinal_arithmetic, cardinal_ordinal}): Ordinals aren't a small type (#11756)

mathlib3
cbad62c5 - feat(set_theory/{ordinal_arithmetic, cardinal_ordinal}): Ordinals aren't a small type (#11756)