mathlib3

46302c70 - refactor(algebra/group/defs): remove left-right_cancel_comm_monoids (#7134)

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. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>