Commit 2022-05-07 04:45 ca1375a5

View on Github →

refactor(algebra/order/monoid_lemmas): reorder the file (#13492) Just like in algebra/order/monoid_lemmas_zero_lt, sort by algebraic assumptions and order assumptions first, then put similar lemmas together. It would be simpler to find duplicates, missing lemmas, and inconsistencies. (There are so many!)

Estimated changes

modified theorem exists_square_le
modified theorem le_mul_of_le_mul_left
modified theorem le_mul_of_le_mul_right
modified theorem le_mul_of_le_of_one_le
modified theorem le_mul_of_one_le_left'
modified theorem le_mul_of_one_le_right'
modified theorem le_of_le_mul_of_le_one_left
modified theorem le_of_mul_le_of_one_le_left
modified theorem lt_mul_of_lt_mul_left
modified theorem lt_mul_of_lt_mul_right
modified theorem lt_mul_of_lt_of_one_le'
modified theorem lt_mul_of_lt_of_one_lt'
modified theorem lt_mul_of_one_le_of_lt
modified theorem lt_mul_of_one_lt_of_lt
modified theorem lt_of_lt_mul_of_le_one_left
modified theorem lt_of_mul_lt_of_one_le_left
modified theorem mul_eq_mul_iff_eq_and_eq
modified theorem mul_eq_one_iff'
modified theorem mul_le_mul'
modified theorem mul_le_mul_left'
modified theorem mul_le_mul_three
modified theorem mul_le_of_le_one_left'
modified theorem mul_le_of_le_one_right'
modified theorem mul_le_of_mul_le_left
modified theorem mul_le_of_mul_le_right
modified theorem mul_left_cancel''
modified theorem mul_lt_mul'''
modified theorem mul_lt_mul_left'
modified theorem mul_lt_mul_of_le_of_lt
modified theorem mul_lt_mul_of_lt_of_le
modified theorem mul_lt_mul_of_lt_of_lt
modified theorem mul_lt_of_le_of_lt_one
modified theorem mul_lt_of_mul_lt_left
modified theorem mul_lt_of_mul_lt_right
modified theorem mul_right_cancel''
modified theorem one_le_mul_right
modified theorem one_lt_mul'
modified theorem one_lt_mul_of_le_of_lt'
modified theorem one_lt_mul_of_lt_of_le'