Transported addition on a uniform pro-p group (source code)

= Transported addition on a uniform pro-p group
{title2=$x+_ny=(x^{p^n}y^{p^n})^{p^{-n}}$}

For a <uniform pro-p group>, the power map $x\mapsto x^{p^n}$ is a <homeomorphism> onto $G^{p^n}$. Transport multiplication back to $G$ by
$$
x+_ny=(x^{p^n}y^{p^n})^{p^{-n}}.
$$
Unique roots make this an associative <group> operation. For odd $p$, <group commutator> collection gives $x+_ny\equiv y+_nx\pmod{G^{p^{n+1}}}$ and $x+_ny\equiv x+_{n-1}y\pmod{G^{p^n}}$. The operations converge to addition in the <Lie algebra of a uniform pro-p group>.