Theorem Cardinal.isRegular_aleph_add_one

Modification history

2026-03-30 08:57
Mathlib/SetTheory/Cardinal/Regular.lean
feat: cof (ω_ (o + 1)) = ℵ_ (o + 1) (#37020)
Added Cardinal.isRegular_aleph_add_oneView on Github →