Affine monoids have unique sums

In this file we show that finitely generated cancellative torsion-free commutative monoids have unique sums. This is a direct corollary of them embedding into ℤⁿ for some n.

@[instance 100]

instance AffineAddMonoid.to_twoUniqueSums {M : Type u_1} [AddCancelCommMonoid M] [AddMonoid.FG M] [HasUniqueDiv M] : TwoUniqueSums M

@[instance 100]

instance AffineMonoid.to_twoUniqueProds {M : Type u_1} [CancelCommMonoid M] [Monoid.FG M] [HasUniqueRoots M] : TwoUniqueProds M