c → a * c ≤ b` (#18367)

Commit

2 years ago

feat(algebra/order/field/basic): `a ≤ b / c → a * c ≤ b` (#18367) A missing lemma, analogous to the existing `div_le_of_nonneg_of_le_mul`

Author

YaelDillies

Parents