[proofplan] We prove the stronger statement that an [algebraically closed field](/page/Algebraically%20Closed%20Field) has no nontrivial finite algebraic extensions. Let $L/k$ be a finite [separable extension](/page/Separable%20Extension) and take an arbitrary element $\alpha \in L$. Its [minimal polynomial](/page/Minimal%20Polynomial) over $k$ is irreducible, and algebraic closedness forces any nonconstant irreducible polynomial over $k$ to be linear. Hence $\alpha \in k$, so every element of $L$ already lies in $k$, and therefore $L=k$. [/proofplan]

[step:Reduce separable closedness to finite separable extensions]Let $k$ be an algebraically closed field. By the definition of a separably closed field, it suffices to prove that every finite separable [field extension](/page/Field%20Extension) $L/k$ satisfies $L=k$. Let $L/k$ be a finite separable extension. Since $L/k$ is a field extension, we regard $k$ as a subfield of $L$.[/step]

[guided]We start from the extension-theoretic definition of separably closed. A field $k$ is separably closed precisely when it has no proper finite separable field extensions. Therefore, to prove that the algebraically closed field $k$ is separably closed, we take an arbitrary finite separable extension $L/k$ and prove that this extension is not proper. Because $L/k$ is a field extension, the inclusion map $k \hookrightarrow L$ identifies each element of $k$ with an element of $L$. Thus the conclusion $L=k$ means that every element of $L$ is already contained in this embedded copy of $k$.[/guided]

[step:Show each element has a linear minimal polynomial]Let $\alpha \in L$ be arbitrary. Since $L/k$ is finite, $\alpha$ is algebraic over $k$. Let $m_{\alpha,k} \in k[x]$ denote the monic minimal polynomial of $\alpha$ over $k$. Then $m_{\alpha,k}$ is irreducible in $k[x]$ and satisfies $m_{\alpha,k}(\alpha)=0$. If $m_{\alpha,k}$ is constant, then it cannot vanish at $\alpha$, because the only constant polynomial that vanishes is the zero polynomial, and the minimal polynomial is nonzero. Hence $m_{\alpha,k}$ is nonconstant. Since $k$ is algebraically closed, $m_{\alpha,k}$ has a root $a \in k$. Therefore $x-a$ divides $m_{\alpha,k}$ in $k[x]$. Because $m_{\alpha,k}$ is irreducible and $x-a$ is nonconstant, the divisor $x-a$ must be an associate of $m_{\alpha,k}$. Since $m_{\alpha,k}$ is monic, this gives \begin{align*} m_{\alpha,k}=x-a. \end{align*} Evaluating at $\alpha$ gives $\alpha-a=0$, so $\alpha=a \in k$.[/step]

[guided]Fix an element $\alpha \in L$. The point of looking at one element is that field equality can be tested elementwise: if every $\alpha \in L$ lies in $k$, then $L \subset k$. Because $L/k$ is finite, every element of $L$ is algebraic over $k$. Thus $\alpha$ has a monic minimal polynomial over $k$, which we denote by $m_{\alpha,k} \in k[x]$. By definition, $m_{\alpha,k}$ is the unique monic polynomial of least positive degree in $k[x]$ satisfying \begin{align*} m_{\alpha,k}(\alpha)=0. \end{align*} It is irreducible in $k[x]$; otherwise a proper nonconstant factor vanishing at $\alpha$ would contradict minimality. The polynomial $m_{\alpha,k}$ is nonconstant. Indeed, a constant nonzero polynomial cannot vanish at $\alpha$, while the zero polynomial is not allowed as a minimal polynomial. Since $k$ is algebraically closed, every nonconstant polynomial in $k[x]$ has a root in $k$. Applying this to $m_{\alpha,k}$, choose $a \in k$ such that \begin{align*} m_{\alpha,k}(a)=0. \end{align*} By the [factor theorem](/theorems/3235) in $k[x]$, the equality $m_{\alpha,k}(a)=0$ implies that $x-a$ divides $m_{\alpha,k}$. Now $m_{\alpha,k}$ is irreducible, and $x-a$ is a nonconstant divisor. Therefore the divisor cannot be proper: $x-a$ is an associate of $m_{\alpha,k}$. Since $m_{\alpha,k}$ was chosen monic, the unit factor is $1$, so \begin{align*} m_{\alpha,k}=x-a. \end{align*} Finally, evaluating the identity $m_{\alpha,k}(\alpha)=0$ gives \begin{align*} \alpha-a=0. \end{align*} Thus $\alpha=a$, and since $a \in k$, we conclude $\alpha \in k$.[/guided]

[step:Conclude that the extension is trivial] The element $\alpha \in L$ was arbitrary, so every element of $L$ belongs to $k$. Hence $L \subset k$. Since $L/k$ is a field extension, $k \subset L$. Therefore $L=k$. Thus every finite separable extension of $k$ is equal to $k$, so $k$ is separably closed. This proves that every algebraically closed field is separably closed. [/step]