Theorem Cardinal.IsRegular.ne_zero

Modification history

2025-03-11 00:25

Mathlib/SetTheory/Cardinal/Cofinality.lean

chore(SetTheory/Cardinal/Cofinality): split file (#21972) …

Modified Cardinal.IsRegular.ne_zero View on Github →

2025-02-13 14:43

Mathlib/SetTheory/Cardinal/Cofinality.lean

feat(SetTheory): regular cardinals have a least element (#21780) …

Added Cardinal.IsRegular.ne_zero View on Github →