Lubin–Tate functional equation lemma (source code)

= Lubin–Tate functional equation lemma
{c}

Given Lubin–Tate series $f,g$ for $\pi$ and a linear form $L=\sum a_iX_i$, there is a unique power series $F\equiv L$ modulo terms of degree two satisfying
$$
f(F(X_1,\ldots,X_n))=F(g(X_1),\ldots,g(X_n)).
$$
Comparison degree by degree determines each homogeneous term; the Lubin–Tate congruences provide the required divisibility by $\pi$.