Commit 2022-03-03 17:48 ba998da9

View on Github →

feat(algebra/order/monoid_lemmas_zero_lt): more lemmas using pos_mul and friends (#12355) This PR continues the order refactor. The added lemmas are the \le analogues of the < lemmas that are already present.

Estimated changes

Modified src/algebra/order/monoid_lemmas_zero_lt.lean

added theorem zero_lt.le_of_mul_le_mul_left'

added theorem zero_lt.le_of_mul_le_mul_right'

added theorem zero_lt.lt_of_mul_lt_mul_left''

added theorem zero_lt.lt_of_mul_lt_mul_right''

added theorem zero_lt.mul_le_mul_iff_left

added theorem zero_lt.mul_le_mul_iff_right

added theorem zero_lt.mul_le_mul_left'

added theorem zero_lt.mul_le_mul_right'