feat(algebra/group/defs): add is_cancel_mul (#17440)
We add a class `is_cancel_mul` (and also other related classes). In a following PR we will take care of `is_cancel_mul_with_zero`, the goal is to redefine `is_domain` as a cancellative `monoid_with_zero` to be able to consider semirings (where not having zero divisors is not equivalent to being cancellative).
Corresponding mathlib4 PR is [#606](https://github.com/leanprover-community/mathlib4/pull/606).
