A finitely generated torsion-free module over a PID is free.
If , then is free of rank 0. Now assume . Let be a finite set of nonzero generators of . If , then () if and only if since is torsion-free.
Consequently, there is a nonempty subset of that is maximal with respect to the property:
The submodule generated by is clearly a free -module with basis . If , then by maximality there exist , not all zero, such that . Then . Furthermore since otherwise for every .
Since is finite, there exists a nonzero (namely ) such that is contained in :
If , then since . If , then clearly since is generated by .
Therefore, . The map given by is an -module homomorphism with image . Since is torsion-free , hence . Since a submodule of a free module over a PID is free, this proves is free.