Theorem Cardinal.mul_lt_of_lt

Modification history

2026-05-11 11:22
Mathlib/SetTheory/Cardinal/Arithmetic.lean
chore: golf `Cardinal.isRegular_succ` (#36930) …
Modified Cardinal.mul_lt_of_ltView on Github →
2023-02-23 13:50
Mathlib/SetTheory/Cardinal/Ordinal.lean
feat: port SetTheory.Cardinal.Ordinal (#2463)
Added Cardinal.mul_lt_of_ltView on Github →