 Finitely generated torsion-free module over a principal ideal domain

Every finitely generated torsion-free module over a principal ideal domain is free. In the structure theorem, torsion-freeness removes every cyclic torsion summand and leaves only the free summand.