Commit 2022-03-06 07:44 64d953a1

View on Github →

refactor(set_theory/ordinal): enum_lt → enum_lt_enum (#12469) That way, the theorem name matches that of enum_le_enum, typein_lt_typein, and typein_le_typein.

Estimated changes

Modified src/set_theory/ordinal.lean

deleted theorem ordinal.enum_lt

added theorem ordinal.enum_lt_enum

Modified src/set_theory/ordinal_arithmetic.lean