Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-07 10:15 37783539

View on Github →

feat(set_theory/ordinal_arithmetic): enum_ord univ = id (#12391)

Estimated changes

modified theorem ordinal.enum_ord_range
added theorem ordinal.enum_ord_univ
added theorem ordinal.range_enum_ord