Theorem Ordinal.lt_mul_iff_div_lt

Modification history

2026-02-27 10:47
Mathlib/SetTheory/Ordinal/Arithmetic.lean
refactor: nicer definition for ordinal division (#35849) …
Added Ordinal.lt_mul_iff_div_ltView on Github →