Commit 2026-03-21 21:50 d32c79b6

View on Github →

chore: OrderIso.cof_eq → OrderIso.cof_congr (#36898) As suggested by Yaël at https://github.com/leanprover-community/mathlib4/pull/36703#discussion_r2963540858.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

added theorem OrderIso.cof_congr

deleted theorem OrderIso.cof_eq

added theorem OrderIso.lift_cof_congr

deleted theorem OrderIso.lift_cof_eq