Theorem Cardinal.ne_zero_of_isSuccLimit

Modification history

2024-09-18 06:51

Mathlib/SetTheory/Cardinal/Basic.lean

chore(SetTheory/Cardinal/Basic): `Cardinal.IsLimit` → `IsSuccLimit` (#16899)

Added Cardinal.ne_zero_of_isSuccLimit View on Github →