feat(algebra/group/basic): mul_left_eq_self etc (#1446)
feat(algebra/group/basic): mul_left_eq_self etc (#1446)

Simp-lemmas for groups of the form a * b = b ↔ a = 1.
leanprover-community/mathlib,leanprover-community/mathlib