Herbrand quotient of the local multiplicative group ($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.