Give the generator weight one and weight . For , let be the -span of
The identities
and
together with the filtration inequalities show that the definition is independent of how an element is expanded and that
Completeness and an Ordered basis of a complete p-valued group give separatedness through unique noncommutative power-series expansions. This is the Lazard filtration on a group algebra.
Multiplication by induces a central degree-one element , so is a graded -algebra. Sending the initial form of to the initial form of respects the Lie bracket, since the displayed algebra commutator has leading term represented by . The universal property of the universal enveloping algebra therefore gives the Lazard enveloping-algebra map
It is surjective because the defining filtered pieces are spanned by products of and the elements .
For the principal congruence subgroup of , let , , and . In the group algebra,
The factor is congruent to one in filtration degree zero. Direct matrix multiplication, now applied to the group commutator, gives
Consequently modulo . The same argument starts from
Using in the two matrix commutators gives
Since the prefactors may again be replaced by one at this precision, we obtain
Therefore