Torsion-free module over a principal ideal domain is flat (source code)

= Torsion-free module over a principal ideal domain is flat

Over a <principal ideal> domain, a <module> is flat exactly when it is torsion-free. Hence the <tensor product> of two torsion-free <modules> over a <principal ideal> domain is torsion-free: both tensor functors are exact, so their composite is exact.