Theorem Ordinal.nmul_le_nmul_left

Modification history

2025-11-22 20:23
Mathlib/SetTheory/Ordinal/NaturalOps.lean
chore: rename `mul_le_mul_right'` to `mul_le_mul_left` (#30242)
Modified Ordinal.nmul_le_nmul_leftView on Github →
2024-08-27 20:26
Mathlib/SetTheory/Ordinal/NaturalOps.lean
feat(SetTheory/Ordinal/NaturalOps): fix bad names (#15992) …
Added Ordinal.nmul_le_nmul_leftView on Github →