Compositional inverse of a formal power series (source code)

= Compositional inverse of a formal power series
{title2=$f(T)=a_1T+O(T^2),\quad a_1\in R^\times$}

A <formal power series> with zero constant coefficient has a compositional inverse over $R$ exactly when its linear coefficient is a unit. Starting with $b_1=a_1^{-1}$, the degree-$k$ coefficient of $f(b_1T+\cdots+b_kT^k)$ is $a_1b_k$ plus an expression already determined by lower coefficients, so recursion gives a unique inverse. For a homomorphism of <formal group laws>, cancellation in the homomorphism identity proves that this inverse is also a formal-group homomorphism.