Torsion-free cancellative commutative monoid (source code)

= Torsion-free cancellative commutative monoid
{title2=$na=nb\implies 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>.