Torsion-free cancellative commutative monoid ($na=nb⟹a=b$)

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.