Any finite unramified extension of local fields $L/K$ induces a separable extension of residue fields $\ell/k$

Let $L/K$ be a finite unramified extension of non-Archimedean local fields with rings of integers $\mathcal O_L$ and $\mathcal O_K$, maximal ideals $\mathfrak m_L$ and $\mathfrak m_K$, and residue fields $\ell=\mathcal O_L/\mathfrak m_L$ and $k=\mathcal{O}_K/\mathfrak{m}_K$, then a paper I read assumed that $\ell$ must be a simple extension of $k$, i.e. there exists some $\bar{x}\in\ell$ such that $k(\bar{x})=\ell$, and so I presume that it is the case that $\ell/k$ is separable.

But why is this true?

• Isn't the residue field necessarily finite? – sharding4 May 22 '17 at 0:25
• I don't believe so. Consider $\Bbb C(\!(x)\!)$, which has residue field $\Bbb C$ with the usual valuation. In fact, the residue field of $k(\!(x)\!)$ will be $k$ for any field $k$. – Monstrous Moonshine May 22 '17 at 1:03
• Wikipedia says "There is an equivalent definition of non-Archimedean local field: it is a field that is complete with respect to a discrete valuation and whose residue field is finite." And similarly Wolfram Mathworld "A field which is complete with respect to a discrete valuation is called a local field if its field of residue classes is finite." – sharding4 May 22 '17 at 1:12
• Is there any nice source for a proof of that? – Monstrous Moonshine May 22 '17 at 16:22
• This post, math.stackexchange.com/a/252990/254075, references Proposition 1 in Section 1 of Chapter II of Serre's Local Fields. – sharding4 May 22 '17 at 16:52