Commit 2026-03-23 09:51 8a12e932

View on Github →

refactor: IsRegular.cof_eq → IsRegular.cof_ord (#37016)

Estimated changes

Modified Mathlib/CategoryTheory/ObjectProperty/LimitsClosure.lean

Modified Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean

Modified Mathlib/SetTheory/Cardinal/Pigeonhole.lean

Modified Mathlib/SetTheory/Cardinal/Regular.lean

deleted theorem Cardinal.IsRegular.cof_eq

added theorem Cardinal.IsRegular.cof_ord