Solution (source code)

= Solution

The <structure theorem for finitely generated modules over a principal ideal domain> applies to a <Euclidean domain> because every <Euclidean domain> is a <principal ideal domain>. In invariant-factor form, every <finitely generated module> $M$ has a decomposition
$$
\boxed{M\cong R^r\oplus R/(d_1)\oplus\cdots\oplus R/(d_s),\qquad
 d_1\mid d_2\mid\cdots\mid d_s,}
$$
where $r\geq0$, and each $d_i$ is a nonzero <nonunit>. The <rank of a module> $r$ is unique and the <invariant factors of a finitely generated module> $d_i$ are unique up to multiplication by units. The zero module is allowed by taking $r=s=0$.

Every <abelian group> is a <module> over $\mathbb Z$, and a <finite abelian group> is finitely generated. Since $\mathbb Z$ is a <Euclidean domain>, the theorem applies. A nonzero <free module> summand would be infinite, so a finite group has $r=0$. Choosing positive integer representatives gives the finite abelian classification
$$
\boxed{A\cong\mathbb Z/d_1\mathbb Z\oplus\cdots\oplus\mathbb Z/d_s\mathbb Z,
\qquad 2\leq d_1\mid\cdots\mid d_s.}
$$
The ordered integers $d_i$ are uniquely determined. Splitting each $d_i$ into prime powers using the <Chinese remainder theorem> gives the equivalent elementary-divisor form as a direct sum of cyclic prime-power groups.