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]
[IsAddTorsionFree M]
:
@[instance 100]
instance
AffineMonoid.to_twoUniqueProds
{M : Type u_1}
[CancelCommMonoid M]
[Monoid.FG M]
[IsMulTorsionFree M]
: