Commit 2026-04-07 10:05 f7bc94df

View on Github →

feat(SetTheory/Cardinal/Cofinality): cof (a * b) = cof b (#37022) We also tag isSuccLimit_omega0 as simp, so that simp can solve goals like (ω_ ω).cof = ω or cof (x * ω) = ω.

Estimated changes

modified theorem Ordinal.cof_add
added theorem Ordinal.cof_mul