Theorem Cardinal.isRegular_cof

Modification history

2026-03-23 01:32
Mathlib/SetTheory/Cardinal/Regular.lean
feat: cof α < ℵ₀ ↔ cof α ≤ 1 (#36976)
Modified Cardinal.isRegular_cofView on Github →
2025-07-11 17:39
Mathlib/SetTheory/Cardinal/Regular.lean
refactor(SetTheory/Ordinal/Arithmetic): `Ordinal.IsLimit` → `Order.IsSuccLimit` (#26643) …
Modified Cardinal.isRegular_cofView on Github →
2025-03-11 00:25
Mathlib/SetTheory/Cardinal/Cofinality.lean
chore(SetTheory/Cardinal/Cofinality): split file (#21972) …
Modified Cardinal.isRegular_cofView on Github →
2023-02-24 13:27
Mathlib/SetTheory/Cardinal/Cofinality.lean
feat port: SetTheory.Cardinal.Cofinality (#2479)
Added Cardinal.isRegular_cofView on Github →