Decomposition of a group element into p'- and p-parts

Let $p$ be a prime and let $G$ be a finite group, written multiplicatively, and let $g \in G$. Then there exist elements $g', u \in G$ such that $g' u = g$; $g'$ and $u$ commute; the order of $g'$ is coprime to $p$; there is a natural number $a$ with $u^{p^a} = 1$; and both $g'$ and $u$ lie in the subgroup $\langle g\rangle$ of integer powers of $g$ (Subgroup.zpowers g). Thus every element of a finite group factors as a product of a commuting pair consisting of an element of order prime to $p$ and an element of $p$-power order, both of them powers of the original element. The statement asserts existence only; no uniqueness of the pair $(g', u)$ is claimed, and the exponent $a$ is not tied to the $p$-adic valuation of the order of $g$.

This is the classical decomposition of an element of a finite group into its $p$-regular ($p'$-) part $g_{p'}$ and its $p$-part $g_p$, the group-theoretic analogue of a Jordan decomposition. It is used in Rep.eq_zero_of_forall_sum_mul_finrank_hom_res_eq_zero, where trace identities valid on $p$-regular elements in characteristic $p$ are propagated to all elements of the group.