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 $|G|=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\}.$ 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 $|G\times H|=|G|\,|H|$. (For finite groups $G$ and $H$, $|G\times H|=|G|\,|H|$).

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