Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-12 12:05 8284c00e

View on Github →

feat(algebra/order/monoid_lemmas_zero_lt): add missing lemmas (#14770)

Estimated changes

Modified src/algebra/order/monoid_lemmas_zero_lt.lean

added theorem zero_lt.lt_mul_of_one_lt_left

added theorem zero_lt.lt_mul_of_one_lt_right

added theorem zero_lt.mul_lt_of_lt_one_left

added theorem zero_lt.mul_lt_of_lt_one_right