Existence and uniqueness of unramified local extensions (source code)

= Existence and uniqueness of unramified local extensions

For a non-Archimedean <local field> $K$, every finite extension $\ell/k_K$ of its <residue field> is realized by an <unramified extension> of $K$, unique up to $K$-isomorphism. Lift the irreducible polynomial of a residue generator to a monic integral polynomial and adjoin a root. Its residue degree equals its field degree, forcing ramification index one. In any other such extension the <Hensel lemma> lifts the same simple residue root, giving an isomorphism.