Surjectivity of unit norms in unramified extensions (source code)

= Surjectivity of unit norms in unramified extensions
{title2=$N_{L/K}(\mathcal O_L^\times)=\mathcal O_K^\times$}

For a finite <unramified extension> of non-Archimedean <local fields>, the <field norm> on residue units is surjective: on a cyclic group of order $q^n-1$ it is exponentiation by $(q^n-1)/(q-1)$ and has image of order $q-1$. For a common <uniformizer> $\pi$ and $r\geq1$, expansion of the conjugate product gives
$$
N_{L/K}(1+\pi^r a)\equiv1+\pi^r\operatorname{Tr}_{k_L/k_K}(\bar a)\pmod{\pi^{r+1}}.
$$
The <field trace> of a finite <finite field> extension is onto: its polynomial $X+X^q+\cdots+X^{q^{n-1}}$ is nonzero of degree below $q^n$, so defines a nonzero linear map to the base field. Lift a residue norm and correct successively with elements of $1+\pi^r\mathcal O_L$. The infinite product converges by <completeness>, and its norm is the prescribed unit. This argument also works in positive characteristic and when $p$ divides $n$.