mathlib

6e136177 - feat(set_theory/ordinal/basic): better definitions for `0` and `1` (#14651)

feat(set_theory/ordinal/basic): better definitions for `0` and `1` (#14651) We define the `0` and `1` ordinals as the order types of the empty relation on `pempty` and `punit`, respectively. These definitions are definitionally equal to the previous ones, yet much clearer, for two reasons: - They don't make use of the auxiliary `Well_order` type. - Much of the basic API for these ordinals uses this def-eq anyways.