Solution (source code)

= Solution

In this one-dimensional setting, a commutative <formal group law> over a commutative <ring> $R$ is a <formal power series> $F(X,Y)\in R[[X,Y]]$ with
$$
F(X,0)=X,\quad F(0,Y)=Y,\quad F(X,Y)=F(Y,X),\quad
F(F(X,Y),Z)=F(X,F(Y,Z)).
$$
In particular $F(X,Y)=X+Y+$ terms of total degree at least two. There is a unique <formal inverse> $i_F(T)=-T+O(T^2)$; coefficient recursion solves $F(T,i_F(T))=0$.

A morphism from <formal group law> $F$ to $G$ is $f(T)\in TR[[T]]$ satisfying
$$
f(F(X,Y))=G(f(X),f(Y)).
$$
The <invertible morphism criterion for formal group laws> is
$$
\boxed{f\text{ is an isomorphism}\quad\Longleftrightarrow\quad f^{\prime}(0)\in R^{\times}.}
$$
Necessity follows by differentiating $g\circ f=T$ at zero for an inverse $g$. Conversely, write $f(T)=a_1T+a_2T^2+\cdots$ with $a_1$ a <unit>. In constructing $g(T)=b_1T+b_2T^2+\cdots$, the coefficient of $T$ fixes $b_1=a_1^{-1}$; at degree $n$, the equation $f(g(T))=T$ has the form $a_1b_n+$ an already known expression $=0$. This determines every $b_n$ over $R$. The same construction gives an inverse on the other side, and uniqueness makes the two inverses agree. Finally apply $g$ to the morphism identity with $X=g(U),Y=g(V)$ to obtain
$$
g(G(U,V))=F(g(U),g(V)).
$$
Thus the inverse is itself a morphism of <formal group laws>, not merely an inverse <formal power series>. Over a general <ring>, nonzero derivative is insufficient: it must be a <unit>.