Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ordinal.zero_eq_type_empty

Modification history

2022-06-10 02:04

src/set_theory/ordinal/basic.lean

feat(set_theory/ordinal/basic): tweak theorems on order type of empty relation (#14650) …

Deleted ordinal.zero_eq_type_empty View on Github →

2017-12-23 10:06

data/ordinal.lean

feat(data/ordinal): mul, div, mod, dvd, sub, power

Added ordinal.zero_eq_type_empty View on Github →