This is an unofficial reimagining of the Archive of Formal Proofs
Finitely Generated Abelian Groupsby Joseph Thommes and Manuel Eberl