then $$[\mathcal{O}_L : \mathcal{O}_K[G]   \omega_2]_{\mathcal{O}_K} =[\mathcal{O}_L : \mathcal{O}_K[G]   \omega_1]_{\mathcal{O}_K}:$$ indeed from $v_2 \equiv v_1 \pmod{\pi_K^{R+1}}$ we obtain $M_k v_1 \equiv M_kv_2 \pmod{\pi_K^{R+1}}$ for every $k$, so the claim follows from Equation .

We turn to the description of a possible algorithm to compute $m(L/K)$. First we claim that one can effectively find a normal basis generator $\omega_0$ of $L/K$. The usual proof of the normal basis theorem (see for example [@MR1878556 Theorem VI.13.1]) shows that there exists a non-zero (and effectively computable) polynomial $p(x_1,\ldots,x_a) \in K[x_1,\ldots,x_a]$ such that all elements $\omega=\sum_{i=1}^a c_i\alpha_i$ in $L$ that do *not* generate a normal basis for $L/K$ satisfy $p(c_1,\ldots,c_a)=0$. Hence it suffices to find a point where $p(x_1,\ldots,x_n)$ does not vanish, and it is enough to try sufficiently many values of $x_1,\ldots,x_n$ to find some $v_0:=(c_1,\ldots,c_n) \in \mathcal{O}_K^n$ for which $p(c_1,\ldots,c_n) \neq 0$. The element $\omega_0 := \omega(v_0) \in \mathcal{O}_L$ is then a normal basis generator for $L/K$. Next we compute the positive integer $R_0$ defined by the equality $[\mathcal{O}_L : \mathcal{O}_K[G]   \omega_0]=\pi_K^{R_0}\mathcal{O}_K$. This can also be done effectively: indeed, it suffices to compute the determinant $$\det\left( v_0 \bigm\vert M_2v_0 \bigm\vert \cdots \bigm\vert M_nv_0 \right)$$ to sufficient $\pi_K$-adic precision to ensure that one can 