Solution (source code)

= Solution

The main theorem of <local class field theory> gives a continuous <Local Artin map>
$$
\operatorname{Art}_K:K^\times\longrightarrow
\operatorname{Gal}(K^{\mathrm{ab}}/K)
$$
with dense image, normalized by sending a <uniformizer> to a chosen <Frobenius>. For every finite abelian extension $L/K$, it induces the <Local Artin reciprocity> isomorphism
$$
K^\times/N_{L/K}(L^\times)\cong\operatorname{Gal}(L/K).
$$
The <existence theorem of local class field theory> says that the finite-index open subgroups of $K^\times$ are exactly the <norm subgroup of a local field extension>[norm subgroups] $N_{L/K}(L^\times)$ for finite abelian extensions $L/K$, and that the extension is uniquely determined inside $K^{\mathrm{ab}}$.

Write $e=e(L/K)$ and $f=f(L/K)$. The valuation of a <field norm> satisfies
$$
v_K(N_{L/K}x)=f\,v_L(x),
$$
so the valuation image of the norm subgroup is $f\mathbb Z$. The exact sequence obtained from $v_K:K^\times\to\mathbb Z$ therefore gives
$$
[K^\times:N_{L/K}(L^\times)]
=f\,[\mathcal O_K^\times:N_{L/K}(\mathcal O_L^\times)].
$$
The left side is $[L:K]=ef$ by <Local Artin reciprocity>. Cancelling $f$ proves
$$
[\mathcal O_K^\times:N_{L/K}(\mathcal O_L^\times)]=e.
$$