Commit 2026-04-07 04:49 fcdb9398

View on Github →

chore: golf Cardinal.lt_power_cof, rename to Cardinal.lt_power_cof_ord (#36926) We rewrite the proof so as to avoid working with unbundled relations, and golf it somewhat in the process. Renames:

Cardinal.lt_power_cof -> Cardinal.lt_power_cof_ord
Cardinal.lt_cof_power -> Cardinal.lt_cof_ord_power

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

added theorem Cardinal.lt_cof_ord_power

deleted theorem Cardinal.lt_cof_power

deleted theorem Cardinal.lt_power_cof

added theorem Cardinal.lt_power_cof_ord