Commit 2026-03-22 04:25 acd9922a

View on Github →

feat: cofinality is idempotent (#36702) We prove this result for Order.cof and deduce the Ordinal.cof version from it.

Estimated changes

added theorem Order.cof_ord_cof
modified theorem Ordinal.cof_cof