Commit 2026-10-21 08:47 7e47a880

View on Github →

refactor: Cardinal.card_le_iff → Ordinal.card_le_iff (#45105) The declaration is Ordinal.card, not Cardinal.card.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Basic.lean

deleted theorem Cardinal.card_le_iff

deleted theorem Cardinal.card_le_of_le_ord

added theorem Ordinal.card_le_iff

added theorem Ordinal.card_le_of_le_ord