Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-28 10:25 bb90598b

View on Github →

feat(set_theory/ordinal/basic): Turn various lemmas into simp (#14075)

Estimated changes

modified theorem ordinal.card_typein
modified theorem ordinal.enum_inj
modified theorem ordinal.enum_le_enum'
modified theorem ordinal.enum_le_enum
modified theorem ordinal.typein_inj