Theorem Cardinal.cof_omega_one

Modification history

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