Theorem Ordinal.cof_eq'

Modification history

2026-10-10 09:42

Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean

chore: delete deprecated declarations to March 2026 (#44240)

Deleted Ordinal.cof_eq'View on Github →

2026-03-15 22:43

Mathlib/SetTheory/Cardinal/Cofinality.lean

refactor: redefine `Order.cof` for a preorder (#35513) …

Modified Ordinal.cof_eq'View on Github →

2025-07-11 17:39

Mathlib/SetTheory/Cardinal/Cofinality.lean

refactor(SetTheory/Ordinal/Arithmetic): `Ordinal.IsLimit` → `Order.IsSuccLimit` (#26643) …

Modified Ordinal.cof_eq'View on Github →

2023-02-24 13:27

Mathlib/SetTheory/Cardinal/Cofinality.lean

feat port: SetTheory.Cardinal.Cofinality (#2479)

Added Ordinal.cof_eq'View on Github →