Commit 2026-03-30 08:57 0a6afa80

View on Github →

feat: cof (ω_ (o + 1)) = ℵ_ (o + 1) (#37020)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

added theorem Cardinal.succ_aleph

added theorem Cardinal.succ_preAleph

Modified Mathlib/SetTheory/Cardinal/Regular.lean

added theorem Cardinal.cof_omega_add_one

added theorem Cardinal.cof_omega_one

added theorem Cardinal.cof_preOmega_add_one

added theorem Cardinal.isRegular_aleph_add_one

modified theorem Cardinal.isRegular_aleph_succ

added theorem Cardinal.isRegular_preAleph_add_one

modified theorem Cardinal.isRegular_preAleph_succ