Commit 2026-05-11 11:22 403f170a

View on Github →

chore: golf Cardinal.isRegular_succ (#36930) We rewrite the proof so as to avoid working with unbundled relations, and golf it somewhat in the process.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Arithmetic.lean

added theorem Cardinal.mul_le_of_le

modified theorem Cardinal.mul_lt_of_lt

Modified Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean

Modified Mathlib/SetTheory/Cardinal/Regular.lean

modified theorem Cardinal.isRegular_succ