Commit 2024-08-27 20:26 977b1348
View on Github →feat(SetTheory/Ordinal/NaturalOps): fix bad names (#15992)
nmul_le_nmul_of_nonneg_left and nmul_le_nmul_of_nonneg_right are dumb since all natural ordinals are non-negative. mul_le_nmul should have been in the ordinal namespace (like add_le_nadd).