Commit 2021-02-14 19:41 22b26d3c

chore(algebra/group/basic): remove three redundant lemmas (#6197) The following lemmas are changed in this PR (long list because of the additive versions:

• mul_eq_left_iff for left_cancel_monoid is renamed to mul_right_eq_self which previously was stated for group
• add_eq_left_iff the additive version is automatically renamed to add_right_eq_self
• mul_eq_right_iff for right_cancel_monoid is renamed to mul_left_eq_self which previously was stated for group
• add_eq_right_iff the additive version is automatically renamed to add_left_eq_self
• left_eq_mul_iff is renamed to self_eq_mul_right to fit the convention above
• left_eq_add_iff is renamed to self_eq_add_right to fit the convention above
• right_eq_mul_iff is renamed to self_eq_mul_left to fit the convention above
• right_eq_add_iff is renamed to self_eq_add_left to fit the convention above
• the duplicate mul_left_eq_self and add_left_eq_self for groups are removed
• the duplicate mul_right_eq_self and add_right_eq_self for groups are removed
• mul_self_iff_eq_one and add_self_iff_eq_zero deal only with the special case a=b of the other lemmas. It is therefore removed and the few instances in the library are replaced by one of the above. While I was at it, I provided a module doc for this file.