Solution (source code)

= Solution

A one-dimensional commutative <formal group law> over $\mathcal O_K$ is a power series $F(X,Y)\in\mathcal O_K[[X,Y]]$ satisfying
$$
F(X,0)=X,
\qquad F(X,Y)=F(Y,X),
\qquad F(F(X,Y),Z)=F(X,F(Y,Z)).
$$
A morphism $h:\mathcal F\to\mathcal G$ is a series $h(T)\in T\mathcal O_K[[T]]$ satisfying
$$
h(F(X,Y))=G(h(X),h(Y)).
$$
If $h(T)=uT+O(T^2)$, the <invertible morphism criterion for formal group laws> says that $h$ is an isomorphism whenever $u\in\mathcal O_K^\times$. Indeed, recursive coefficient comparison constructs a unique compositional inverse $j(T)$; applying $j$ to the morphism identity shows that $j$ is a morphism in the opposite direction.

The multiplication series has
$$
[n]_{\mathcal F}(T)=nT+O(T^2).
$$
Since $p\nmid n$, its linear coefficient is a unit, so $[n]_{\mathcal F}$ is an automorphism of the group $\mathcal F(\pi\mathcal O_K)$. Its kernel is therefore zero, and
$$
\boxed{\mathcal F(\pi\mathcal O_K)[n]=0.}
$$