mathlib3

33fa3e42 - feat(algebra/group/{ unique_prods + to_additive, counterexamples/zero_divisors_in_add_monoid_algebras.lean }): new file and to_additive dictionary (#16329)

feat(algebra/group/{ unique_prods + to_additive, counterexamples/zero_divisors_in_add_monoid_algebras.lean }): new file and to_additive dictionary (#16329) This PR introduces `unique_prods` and `unique_sums`. They correspond to a property called "'unique products" in the context of Kaplansky's conjectures. Zulip discussions: [unique products](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/unique.20products) and [PR review](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2316329.3A.20unique.20products)