Solution (source code)

= Solution

In this setting a <formal group law> means a one-dimensional commutative series $F(X,Y)\in\mathcal O_K[[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)).
$$
These identities force $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)$ with $F(T,i_F(T))=0$.

A morphism to another <formal group law> $G$ is a series $h(T)=cT+O(T^2)$ satisfying $h(F(X,Y))=G(h(X),h(Y))$. The <invertible morphism criterion for formal group laws> is
$$
\boxed{h\text{ is an isomorphism over }\mathcal O_K\iff c\in\mathcal O_K^{\times}.}
$$
Necessity follows by comparing linear coefficients in $h^{-1}\circ h=T$. For sufficiency, solve recursively for a compositional inverse $j(T)=c^{-1}T+\cdots$: at every stage the new coefficient is obtained by dividing by the unit $c$, so all coefficients stay in $\mathcal O_K$. Applying $j$ to the morphism identity shows that $j$ is itself a <group homomorphism> of <formal group laws>.

In particular, the multiplication series satisfies $[n]_F(T)=nT+O(T^2)$. Since $p\nmid n$, the <multiplication isomorphism of a formal group law> makes $[n]_F$ invertible over $\mathcal O_K$. Its series and inverse converge on $\mathfrak m_K$, so multiplication by $n$ is bijective on $E_1(K)$, and on $E_1(L)$ for every finite extension $L/K$.