Theorem Ordinal.nmul_le_nmul

Modification history

2026-02-20 00:22
Mathlib/SetTheory/Ordinal/NaturalOps.lean
chore: remove deprecated material from CGT (#35550) …
Deleted Ordinal.nmul_le_nmulView on Github →
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 →