Mathlib v3 is deprecated. Go to Mathlib v4

Theorem cardinal.succ_zero

Modification history

2022-05-28 04:03

src/set_theory/cardinal/basic.lean

refactor(set_theory/cardinal/*): `cardinal.succ` → `order.succ` (#14273)

Modified cardinal.succ_zero View on Github →

2017-12-19 04:59

data/cardinal.lean

feat(data/ordinal): sup, cofinality, subtraction

Added cardinal.succ_zero View on Github →