Fundamental theorem of finite abelian groups: invariant-factor form

Given: The objects and hypotheses in the statement.

Every finite abelian group is isomorphic to a finite direct product of cyclic groups of prime-power order. The multiset of their orders is uniquely determined by the group, up to permutation of the factors. (Fundamental theorem of finite abelian groups: elementary-divisor form).

Every multiset of prime-power elementary divisors regroups in exactly one way into an invariant-factor list. (Elementary divisors regroup uniquely into invariant factors).

An invariant-factor list for a finite abelian group $G$ is a finite list of integers $1<n_1\mid n_2\mid \cdots \mid n_r$ together with an isomorphism $G\cong C_{n_1}\times \cdots \times C_{n_r}$. The cyclic factors and product use thm-classification-of-cyclic-groups and def-external-direct-product-of-groups. Unit factors are omitted. The trivial group has the empty list. (Invariant-factor data for a finite abelian group).

If $G$ and $H$ are finite groups, then their external direct product is finite and has order $\mathrm{\mid }G\times H\mathrm{\mid }=\mathrm{\mid }G\mathrm{\mid }\mathrm{\mid }H\mathrm{\mid }$. (For finite groups $G$ and $H$, $\mathrm{\mid }G\times H\mathrm{\mid }=\mathrm{\mid }G\mathrm{\mid }\mathrm{\mid }H\mathrm{\mid }$).