Residue-basis norm formula for an unramified extension (source code)

= Residue-basis norm formula for an unramified extension
{title2=$|\sum_j a_jx^j|=\max_j|a_j|$}

Let $L/K$ be a finite <unramified extension> of complete fields with a <Non-Archimedean absolute value>, with separable residue extension and $[L:K]=[k_L:k_K]=n$. If $x$ is integral and its residue generates $k_L/k_K$, then $1,x,\ldots,x^{n-1}$ form a $K$-basis. Divide any nonzero combination by a coefficient of largest absolute value. Its remaining coefficients are integral, at least one is a unit, and the residue-basis independence makes the reduction nonzero. The displayed norm formula follows. In particular, the combination is integral exactly when every coefficient is integral, proving $\mathcal O_L=\mathcal O_K[x]$ without requiring a discrete valuation.