mathlib3

4b240be0 - feat(algebra/group_with_zero/defs): add is_cancel_mul_zero (#17716)

feat(algebra/group_with_zero/defs): add is_cancel_mul_zero (#17716) We add a class `is_cancel_mul_with_zero` (and also other related classes). This is the continuation of #17440. Corresponding mathlib4 PR [#724](https://github.com/leanprover-community/mathlib4/pull/724).