Herbrand quotient of the local multiplicative group (source code)

= Herbrand quotient of the local multiplicative group
{c}
{title2=$h_G(L^\times)=[L:K]$}

For a cyclic extension of <p-adic fields>, sufficiently deep <principal units> are equivariantly isomorphic to an additive lattice by the <p-adic logarithm>. The <normal basis theorem> makes its <Herbrand quotient> one. Passing across finite unit quotients preserves it. The valuation exact sequence with quotient $\mathbb Z$ therefore gives the displayed formula.