mathlib3
d0bf8bd2 - feat(set_theory/ordinal): `ordinal` is a successor order (#11284)

Commit

4 years ago

feat(set_theory/ordinal): `ordinal` is a successor order (#11284) This provides the `succ_order` instance for `ordinal`.

Author

YaelDillies

Parents