Theorem Cardinal.mul_le_of_le

Modification history

2026-05-11 11:22
Mathlib/SetTheory/Cardinal/Arithmetic.lean
chore: golf `Cardinal.isRegular_succ` (#36930) …
Added Cardinal.mul_le_of_leView on Github →