Theorem Ordinal.nmul_le_nmul

Modification history

2025-11-22 20:23
Mathlib/SetTheory/Ordinal/NaturalOps.lean
chore: rename `mul_le_mul_right'` to `mul_le_mul_left` (#30242)
Added Ordinal.nmul_le_nmulView on Github →