mathlib3

a3c647bb - feat(set_theory/ordinal/arithmetic): tweak theorems about `0` and `1` (#15174)

feat(set_theory/ordinal/arithmetic): tweak theorems about `0` and `1` (#15174) We add a few basic theorems on the `0` and `1` ordinals. We rename `one_eq_type_unit` to `type_unit`, and remove `one_eq_lift_type_unit` by virtue of being a trivial consequence of `type_unit` and `lift_one`.