Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-28 21:58 25e7fe6b

View on Github →

chore(algebra/order/monoid_lemmas_zero_lt): reorder, create aliases (#16522) The first part of #16449

Estimated changes

added theorem le_of_mul_le_mul_left
added theorem le_of_mul_le_mul_right
modified theorem lt_of_mul_lt_mul_left
modified theorem lt_of_mul_lt_mul_right
modified theorem mul_le_mul_left
modified theorem mul_le_mul_of_nonneg_left
modified theorem mul_le_mul_of_nonneg_right
modified theorem mul_le_mul_right
modified theorem mul_lt_mul_left
modified theorem mul_lt_mul_of_pos_left
modified theorem mul_lt_mul_of_pos_right
modified theorem mul_lt_mul_right