Solution (source code)

= Solution

A <nilpotent group> has a finite <central series>
$$
1=Z_0\le Z_1\le\cdots\le Z_c=G,\qquad [G,Z_{j+1}]\le Z_j.
$$
Equivalently the <upper central series>, defined by $Z_{j+1}/Z_j=Z(G/Z_j)$, reaches $G$.

We first prove the <normalizer condition for nilpotent groups>. If $H<G$, choose the least $j$ with $Z_j\not\subseteq H$. Then $Z_{j-1}\le H$, and an element $z\in Z_j\setminus H$ satisfies $[z,H]\le Z_{j-1}\le H$. Thus $z$ normalizes $H$, giving $H<N_G(H)$.

Let $P$ be a <Sylow subgroup> of a finite nilpotent $G$, and write $N=N_G(P)$. If $N<G$, the <normalizer> condition gives some $g\in N_G(N)\setminus N$. The <subgroups> $P$ and $P^g$ are both <Sylow subgroups> of $N$, so <Sylow theorem> supplies $n\in N$ with $P^{gn}=P$. But then $gn\in N_G(P)=N$, forcing $g\in N$, a contradiction. Therefore every <Sylow subgroup> is a <normal subgroup> of $G$.

For normal <Sylow subgroups> $P,Q$ at different primes, $[P,Q]\le P\cap Q=1$. They commute, have coprime orders, and their product has order $|G|$. Multiplication consequently gives an isomorphism from their external <direct product of groups> onto $G$.

Conversely, a nontrivial <finite p-group> has nontrivial <center of a group>: its <class equation> has every noncentral conjugacy-class size divisible by $p$, so $|Z(G)|$ is a positive multiple of $p$. Induction on order, applied to $G/Z(G)$, gives a central series for $G$. Finite direct products of these central series give a central series for the product, padding shorter series by the full factor. Thus the <finite nilpotent group decomposition> is
$$
\boxed{G\text{ nilpotent}\ \Longleftrightarrow\
G\cong\prod_{p\mid |G|}P_p.}
$$