Commit 2019-09-16 16:01 b2b0de46
View on Github →feat(algebra/group/basic): mul_left_eq_self etc (#1446) Simp-lemmas for groups of the form a * b = b ↔ a = 1.
feat(algebra/group/basic): mul_left_eq_self etc (#1446) Simp-lemmas for groups of the form a * b = b ↔ a = 1.