Commit 2022-07-08 02:55 a3c647bb
View on Github →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.