Embedding a finitely generated torsion-free module in a finite free module (source code)

= Embedding a finitely generated torsion-free module in a finite free module
{title2=$M\hookrightarrow R^r$}

Apply <clearing denominators relative to an independent module subset> to find $0\ne a$ with $aM$ lying in a <finite free module>. Multiplication by $a$ is injective on a <torsion-free module>, giving the required embedding. A submodule need not itself be free over a general <integral domain>.