Invariant factors determine the order and exponent of a finite abelian group

Given: The objects and hypotheses in the statement.

For every finite abelian group $G$ there is a unique list $1<n_1\mid \cdots \mid n_r$ such that $G\cong C_{n_1}\times \cdots \times C_{n_r}$. Moreover $\mathrm{\mid }G\mathrm{\mid }=n_1\cdots n_r$. The trivial group corresponds to the empty list and empty product. (Fundamental theorem of finite abelian groups: invariant-factor form).

For a finite group $G$, its exponent is $\exp (G)=\min \{n\in \mathbb{N}:n>0\text{ and }{g}^n=e\text{ for every }g\in G\}\mathrm{.}$ The set is nonempty by cor-g-to-the-group-order-is-identity, and thm-well-ordering-principle gives its least member; powers use def-group-power. Thus the definition is well-defined. For the trivial group $\exp (G)=1$. (The exponent of a finite 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 }$).

Let $\iota :\mathbb{N}\to \mathbb{Z}$ be the canonical embedding. If $g\in G$ and $h\in H$ have finite orders $m,n\ge 1$, then in the external direct product $\mathrm{ord}(g,h)=\mathrm{lcm}(m,n)\mathrm{.}$ (If $g$ and $h$ have finite orders $m$ and $n$, then $\iota (\mathrm{ord}(g,h))=\mathrm{lcm}(\iota (m),\iota (n))$ in $G\times H$).