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.