1 files changed, 18 insertions, 5 deletions

diff --git a/chapitres/extensions-algebriques.tex b/chapitres/extensions-algebriques.tex
index 00e4eeb..b246206 100644
--- a/chapitres/extensions-algebriques.tex
+++ b/chapitres/extensions-algebriques.tex
@@ -2170,6 +2170,22 @@ Par définition (\ref{pot-diag-reduit}), $f$ est donc séparable.
 
 \subsection{Clôture séparable}
 
+\begin{proposition2}\label{extension-algebrique-separable-maximale}
+Soit $K\bo k$ une extension algébrique de corps.  L'ensemble $K_0$ des
+éléments de $K$ séparables sur $k$ est une extension algébrique
+séparable de $k$ : c'est la plus grande extension séparable de $k$
+contenue dans $K$.
+\end{proposition2}
+\begin{proof}
+Soient $x,y∈K$ séparables sur $k$. L'extension composée $k(x,y)$ de
+$k(x)$ et $k(y)$ dans $K$ est algébrique séparable sur $k$ d'après
+\ref{compose-etale} de sorte que $x+y$, $xy$, et $x^{-1}$ si $x≠0$,
+sont également séparables sur $k$. L'ensemble $K_0$ est donc un corps,
+contenant $k$ et algébrique séparable sur $k$, et toute extension
+algébrique séparable de $k$ contenue dans $K$ est par définition
+contenue dans $K_0$, de sorte que c'est bien la plus grande.
+\end{proof}
+
 \begin{définition2}
 Un corps $K$ est dit \emph{séparablement clos} 
 si toute extension étale de $K$ est triviale.
@@ -2186,11 +2202,8 @@ sous-corps séparablement clos de $Ω$ contenant $k$.
 \end{proposition2}
 
 \begin{démo}
-Soient $x,y∈Ω$ séparables sur $k$. L'extension 
-composée $k(x,y)$ de $k(x)$ et $k(y)$ dans $Ω$ est algébrique séparable sur $k$ d'après  
-\ref{compose-etale} de sorte que $x+y$, $xy$, et
-$x^{-1}$ si $x≠0$, sont également séparables sur $k$. L'ensemble
-$Ω₀$ est donc un corps, contenant $k$ et algébrique séparable sur $k$.
+D'après \ref{extension-algebrique-separable-maximale}, on sait que
+$Ω₀$ est un corps contenant $k$ et algébrique séparable sur $k$.
 Si $z∈Ω$ est séparable sur $Ω₀$, il est séparable sur une sous-$k$-extension
 \emph{étale} $k'$ de $Ω₀$, par exemple le corps
 engendré sur $k$ par les coefficients du polynôme