Cancellative commutative monoid ($a+c=b+c⟹a=b$)

A commutative monoid is cancellative when $a+c=b+c$ implies $a=b$. Cancellation makes the natural map into its Grothendieck group injective.

A cancellative commutative monoid is torsion-free in this sense when $na=nb$ implies $a=b$ for every positive integer $n$. Its Grothendieck group is then a torsion-free abelian group, because $n(a-b)=0$ forces $na=nb$. This is the condition inherited by a submonoid of a torsion-free abelian group.