Commit 2021-02-17 11:38 9b3008eb

View on Github →

feat(algebra/ordered_monoid): inequalities involving mul/add (#6171) I couldn't find some statements about inequalities, so I'm adding them. I included all the useful variants I could think of.

Estimated changes

Modified src/algebra/ordered_monoid.lean

added theorem le_mul_of_le_mul_left

added theorem le_mul_of_le_mul_right

added theorem le_of_le_mul_of_le_one_left

added theorem le_of_le_mul_of_le_one_right

added theorem le_of_mul_le_of_one_le_left

added theorem le_of_mul_le_of_one_le_right

added theorem lt_mul_of_lt_mul_left

added theorem lt_mul_of_lt_mul_right

added theorem lt_of_lt_mul_of_le_one_left

added theorem lt_of_lt_mul_of_le_one_right

added theorem lt_of_mul_lt_of_one_le_left

added theorem lt_of_mul_lt_of_one_le_right

added theorem mul_le_of_le_one_left'

added theorem mul_le_of_le_one_right'

added theorem mul_le_of_mul_le_left

added theorem mul_le_of_mul_le_right

added theorem mul_lt_of_mul_lt_left

added theorem mul_lt_of_mul_lt_right