Commit 2022-06-29 18:27 397d45f2

View on Github →

feat(algebra/order/monoid): a + b ≤ c → a ≤ c (#15033) Generalize four lemmas that were left by previous PRs before canonically_ordered_monoid was a thing.

Estimated changes

Modified src/algebra/order/monoid.lean

added theorem le_of_mul_le_left

added theorem le_of_mul_le_right

Modified src/data/matrix/rank.lean

Modified src/data/nat/basic.lean

deleted theorem nat.le_of_add_le_left

deleted theorem nat.le_of_add_le_right

Modified src/data/polynomial/coeff.lean

Modified src/data/polynomial/hasse_deriv.lean

Modified src/data/real/nnreal.lean

deleted theorem nnreal.le_of_add_le_left

deleted theorem nnreal.le_of_add_le_right

Modified src/ring_theory/power_series/basic.lean