Solution (source code)

= Solution

Define the <Lubin–Tate torsion> by
$$
\mu_{f,n}=\{x\in\overline{\mathfrak m}:[\pi^n]_f(x)=f^{\circ n}(x)=0\}.
$$
The scalar endomorphisms make this a module over $\mathcal O_K/\pi^n\mathcal O_K$.

The <Newton polygon> or <Weierstrass preparation theorem> applied to the Lubin–Tate congruences shows that $[\pi^n]_f$ has exactly $q^n$ distinct roots in $\overline{\mathfrak m}$. More precisely, the quotient of the distinguished factors for $[\pi^n]_f$ and $[\pi^{n-1}]_f$ has degree $q^{n-1}(q-1)$, and its roots are precisely the points killed by $\pi^n$ but not by $\pi^{n-1}$.

Choose such a point $\omega_n$. If $a\in\mathcal O_K$, write $a=\pi^ru$ with $u$ a <unit>. Since $[u]_f$ is an automorphism, $[a]_f(\omega_n)=0$ exactly when $r\geq n$. Thus
$$
\mathcal O_K/\pi^n\mathcal O_K\longrightarrow\mu_{f,n},
\qquad
a\longmapsto[a]_f(\omega_n),
$$
is injective. Both sides have $q^n$ elements, so it is an isomorphism of modules. Therefore $\mu_{f,n}$ is a <free module> of rank one.