Commit 2023-04-23 07:33 8ad95dbd

View on Github →

chore: forward-port leanprover-community/mathlib#18831 (#3572)

Estimated changes

added theorem div_le_one_of_ge
added theorem le_mul_of_le_one_left
added theorem le_mul_of_le_one_right
added theorem lt_mul_of_lt_one_left
added theorem lt_mul_of_lt_one_right
added theorem mul_le_of_one_le_left
added theorem mul_le_of_one_le_right
added theorem mul_lt_of_one_lt_left
added theorem mul_lt_of_one_lt_right