Unramified residue generator integral basis (source code)

= Unramified residue generator integral basis
{title2=$\mathcal O_L=\bigoplus_{j=0}^{f-1}\mathcal O_K\alpha^j$}

For an <unramified extension> of <local fields> $L/K$, an integral element whose residue generates $k_L/k_K$ generates $L/K$: its degree is at least the <residue degree> $f=[L:K]$. The reduced powers $1,\bar\alpha,\ldots,\bar\alpha^{f-1}$ are a <basis> of the <residue field> extension. If $x=\sum c_j\alpha^j$, factor out a coefficient of least <valuation>. Reduction of the remaining sum is nonzero by that residue <basis>, so $v_L(x)=\min_j v_K(c_j)$. Consequently $x$ is integral exactly when all $c_j$ are integral.