feat: TwoUniqueProds (#7169)

+ Introduce `TwoUniqueProds/Sums`: let `R[G]` be a monoid algebra over a semiring `R` without zero-divisors. A natural sufficient condition for `R[G]` to have no zero-divisors is that `G` has `UniqueProds`, as is shown by [MonoidAlgebra.instNoZeroDivisorsOfUniqueProds](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.html#MonoidAlgebra.instNoZeroDivisorsOfUniqueProds). Similarly, a natural sufficient condition for `R[G]` to have only trivial units (of the form `rg` with `r` a unit in `R` and `g` a unit in `G`) is that `G` has `TwoUniqueProds`, but we don't prove this yet in this PR. `TwoUniqueProds G` is also a natural sufficient condition in order for factors of a homogeneous element in an algebra graded by `G` without zero-divisors to themselves be homogeneous.

+ Show `TwoUniqueProds` implies `UniqueProds`: `TwoUniqueProds.toUniqueProds`

+ Strengthen `of_Covariant_right/left` to have `TwoUniqueProds` as conclusion

+ Extract `of_image_filter` from the proof of the instance `UniqueProds (∀ i, G i)` and use it also in the proof of `TwoUniqueProds (∀ i, G i)`

+ Use some private defs (starting from `private abbrev I`) to transfer `(Two)UniqueProds (∀ i, G i)` instances to `(Two)UniqueProds (G × H)`

+ Move the `[Module ℚ G] : UniqueSums G` instance from NoZeroDivisors.lean to UniqueProds.lean and strengthen to `TwoUniqueSums`

New lemmas about UniqueMul:
+ `of_card_le_one`, `iff_card_le_one`, `UniqueMul_of_TwoUniqueMul`



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>