Structure theorem for finitely generated modules over a PID

Structure theorem (f.g. modules over a PID): Let $R$ be a principal ideal domain and let $M$ be a finitely generated module over $R$. Then there exist an integer $r\ge 0$ and nonzero elements $d_1,\dots,d_t\in R$ with $d_1\mid d_2\mid \cdots \mid d_t$ such that

a decomposition as a direct sum of a free part and cyclic torsion factors. The integer $r$ and the invariant factors $d_i$ are unique up to multiplication by units in $R$. In particular, the torsion submodule of $M$ is a torsion module and the free summand is a free module of rank $r$.

This theorem is the module-theoretic engine behind the classification of finitely generated abelian groups (the case $R=\mathbb Z$); see classification of finitely generated abelian groups. It is closely tied to Smith normal form, and it admits an equivalent primary decomposition form (see the elementary divisor theorem).