Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ordinal.ne_zero_of_out_nonempty

Modification history

2022-07-06 21:58
src/set_theory/ordinal/basic.lean
chore(set_theory/ordinal/basic): clean up `ordinal.card` API (#15147) …
Added ordinal.ne_zero_of_out_nonemptyView on Github →