Commit 2021-04-12 23:25 46302c70

refactor(algebra/group/defs): remove left-right_cancel_comm_monoids (#7134) There were 6 distinct classes

• (add_)left_cancel_comm_monoid,
• (add_)right_cancel_comm_monoid,
• (add_)cancel_comm_monoid. I removed them all, except for the last 2:
• (add_)cancel_comm_monoid. The new typeclass cancel_comm_monoid requires only a * b = a * c → b = c, and deduces the other version from commutativity.