Theorem Ordinal.cof_cof

Modification history

2026-03-23 03:33
Mathlib/SetTheory/Cardinal/Cofinality.lean
chore: rename `Ordinal.cof_cof` → `Ordinal.cof_ord_cof` (#36975) …
Deleted Ordinal.cof_cofView on Github →
2026-03-22 04:25
Mathlib/SetTheory/Cardinal/Cofinality.lean
feat: cofinality is idempotent (#36702) …
Modified Ordinal.cof_cofView on Github →
2023-02-24 13:27
Mathlib/SetTheory/Cardinal/Cofinality.lean
feat port: SetTheory.Cardinal.Cofinality (#2479)
Added Ordinal.cof_cofView on Github →