Commit 2026-03-23 03:33 33896e05

View on Github →

chore: rename Ordinal.cof_cof → Ordinal.cof_ord_cof (#36975) As suggested by Yaël in #36702.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

deleted theorem Ordinal.cof_cof

added theorem Ordinal.cof_ord_cof

Modified Mathlib/SetTheory/Cardinal/Regular.lean