and noticing that $b {\leqslant}\frac{a+e_{L/K}-1}{e_{L/K}}$, we obtain $$\begin{aligned}
m(L/K) & {\leqslant}\left[  \mathfrak{B} : \mathcal{O}_K[G] \right] \cdot \frac{ p^{f_K |G| b} }{p^{af_L}} \\
& {\leqslant}\left[  \mathfrak{B} : \mathcal{O}_K[G] \right] \cdot  p^{f_K f_{L/K}e_{L/K} \frac{a+e_{L/K}-1}{e_{L/K}} - af_L} \\
& = \left[  \mathfrak{B} : \mathcal{O}_K[G] \right] \cdot  p^{f_L (e_{L/K}-1)}.
\end{aligned}$$ Using Equation we then obtain $$\begin{aligned}
v_p (m(L/K)) & {\leqslant}f_L(e_{L/K}-1) + \frac{1}{2} [K:\mathbb{Q}_p] \cdot  |G| \cdot v_p(|G|) \\
& = f_L(e_{L/K}-1) +  \frac{1}{2} [L:\mathbb{Q}_p] v_p([L:K]).
\end{aligned}$$ This proves Theorem \[thm:IntroGeneralBound\], and it is clear that one can get a very simple (albeit rough) estimate by replacing $f_L(e_{L/K}-1)$ with $[L:\mathbb{Q}_p]$, thus obtaining $$\label{eq:EasierBound}
v_p(m(L/K)) < [L:\mathbb{Q}_p] (1 + \frac{1}{2} v_p([L:K])).$$

\[rmk:AlmostOptimalBound\] Comparison with cases in which we can compute $m(L/K)$ exactly suggests that the bound of Theorem \[thm:IntroGeneralBound\] is *sharper* when $L/K$ is highly ramified. In fact, in some maximally ramified cases our bound is almost optimal: take for example $K=\mathbb{Q}_p(\zeta_{p^r})$ and $L=K(\sqrt[p^r]{\pi_K})$. One may show that $v_p(m(L/K))=\frac{r}{2} [L:\mathbb{Q}_p]$ (see Remark \[rmk:KummerDegreepn\]), while our result – in the form of Equation – gives the upper bound $\left(\frac{r}{2}+1\right) [L:\mathbb{Q}_p]$, which is essentially sharp for large $r$. Theorem \[thm:IntroGeneralBound\] might thus be useful in situations where a complicated ramification structure prevents the use of other tools.

Reduction 