Lazard enveloping-algebra map (source code)

= Lazard enveloping-algebra map
{c}

The initial form of $g-1$ depends only on the initial form of $g$ in $\operatorname{gr}G$. The resulting Lie map extends to a surjective graded algebra homomorphism
$$
U_{\mathbb F_p[t]}(\operatorname{gr}G)\twoheadrightarrow\operatorname{gr}\mathbb Z_p[G].
$$
For a complete finite-rank p-valued group, ordered-basis expansions show that it is an isomorphism.