Theorem Cardinal.IsRegular.cof_eq

Modification history

2026-03-23 09:51

Mathlib/SetTheory/Cardinal/Regular.lean

refactor: `IsRegular.cof_eq` → `IsRegular.cof_ord` (#37016)

Deleted Cardinal.IsRegular.cof_eq View on Github →

2025-03-11 00:25

Mathlib/SetTheory/Cardinal/Cofinality.lean

chore(SetTheory/Cardinal/Cofinality): split file (#21972) …

Modified Cardinal.IsRegular.cof_eq View on Github →

2023-02-24 13:27

Mathlib/SetTheory/Cardinal/Cofinality.lean

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

Added Cardinal.IsRegular.cof_eq View on Github →