Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ordinal.typein_inj

Modification history

2022-05-28 10:25

src/set_theory/ordinal/basic.lean

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

Modified ordinal.typein_inj View on Github →

2017-12-11 05:07

data/ordinal.lean

feat(data/ordinal): more ordinals

Added ordinal.typein_inj View on Github →