Theorem Ordinal.nmul_le_nmul_of_nonneg_right

Modification history

2024-08-27 20:26
Mathlib/SetTheory/Ordinal/NaturalOps.lean
feat(SetTheory/Ordinal/NaturalOps): fix bad names (#15992) …
Deleted Ordinal.nmul_le_nmul_of_nonneg_rightView on Github →
2023-07-18 05:18
Mathlib/SetTheory/Ordinal/NaturalOps.lean
chore: forward port #14324 (#5973) …
Added Ordinal.nmul_le_nmul_of_nonneg_rightView on Github →