Commit 2026-05-10 20:52 0bb58f28

View on Github →

feat: Order.cof Ordinal = univ (#37675)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean

added theorem Order.cof_cardinal

added theorem Order.cof_ordinal