Power lifting in a powerful p-group (source code)

= Power lifting in a powerful p-group
{title2=$G^p=\{x^p:x\in G\}$}

For odd $p$, set $P_0=G$ and $P_{i+1}=P_i^p$. Powerful embedding gives $[P_i,G]\leq P_{i+1}$. Modulo $P_{i+2}$, commutators with $P_i$ are central and have exponent dividing $p$, so $(xy)^p\equiv x^py^p$ when $y\in P_i$. Also the power map $P_i/P_{i+1}\to P_{i+1}/P_{i+2}$ is a surjective <homomorphism>. First find a root modulo $P_2$, then multiply it by successive corrections in $P_i$. The process terminates for a <finite p-group>, and converges for a <pro-p group> with separated power filtration. This proves that the generated power <subgroup> consists of actual powers.