[proofplan] The separable degree $[L : k]_s$ of a finite extension $L/k$ equals the number of distinct $k$-embeddings $L \hookrightarrow \overline{k}$. We prove multiplicativity by a two-stage counting argument: each $k$-embedding $K \hookrightarrow \overline{k}$ restricts to a $k$-embedding $F \hookrightarrow \overline{k}$, and for each fixed $k$-embedding $\sigma: F \hookrightarrow \overline{k}$, the number of extensions to $K$ is exactly $[K : F]_s$. The product formula follows. The "in particular" statement then follows from the identity $[L : k]_s = [L : k]$ characterising separability. [/proofplan] [step:Recall the definition of separable degree via embeddings] For a finite extension $L/k$, the separable degree $[L : k]_s$ is defined as the number of distinct $k$-algebra homomorphisms $L \hookrightarrow \overline{k}$, i.e., field homomorphisms $\sigma: L \to \overline{k}$ satisfying $\sigma|_k = \operatorname{id}_k$. Such maps are called $k$-embeddings. Since $L/k$ is algebraic, every $k$-algebra homomorphism $L \to \overline{k}$ is injective (a field homomorphism has trivial kernel), so these are indeed embeddings. The extension $L/k$ is separable if and only if $[L : k]_s = [L : k]$. [/step] [step:Partition the $k$-embeddings of $K$ by their restriction to $F$] Let $\operatorname{Emb}_k(K, \overline{k})$ denote the set of $k$-embeddings $K \hookrightarrow \overline{k}$, so $|\operatorname{Emb}_k(K, \overline{k})| = [K : k]_s$. Define the restriction map \begin{align*} \operatorname{res}: \operatorname{Emb}_k(K, \overline{k}) &\to \operatorname{Emb}_k(F, \overline{k}) \\ \tau &\mapsto \tau|_F. \end{align*} This is well-defined: if $\tau: K \hookrightarrow \overline{k}$ fixes $k$ pointwise, then $\tau|_F: F \hookrightarrow \overline{k}$ also fixes $k$ pointwise. The fibres of $\operatorname{res}$ partition $\operatorname{Emb}_k(K, \overline{k})$. For each $\sigma \in \operatorname{Emb}_k(F, \overline{k})$, the fibre is \begin{align*} \operatorname{res}^{-1}(\sigma) = \{\tau \in \operatorname{Emb}_k(K, \overline{k}) : \tau|_F = \sigma\}. \end{align*} Therefore \begin{align*} [K : k]_s = \sum_{\sigma \in \operatorname{Emb}_k(F, \overline{k})} |\operatorname{res}^{-1}(\sigma)|. \end{align*} [guided] We define the restriction map $\operatorname{res}: \operatorname{Emb}_k(K, \overline{k}) \to \operatorname{Emb}_k(F, \overline{k})$ by $\tau \mapsto \tau|_F$. This is well-defined because restricting a $k$-embedding of $K$ to the subfield $F$ gives a $k$-embedding of $F$ (the identity on $k$ is preserved). The key structural observation: the set $\operatorname{Emb}_k(K, \overline{k})$ decomposes as the disjoint union of the fibres $\operatorname{res}^{-1}(\sigma)$ over all $\sigma \in \operatorname{Emb}_k(F, \overline{k})$. This gives \begin{align*} [K : k]_s = |\operatorname{Emb}_k(K, \overline{k})| = \sum_{\sigma \in \operatorname{Emb}_k(F, \overline{k})} |\operatorname{res}^{-1}(\sigma)|. \end{align*} To obtain the product formula, we need to show two things: (1) the restriction map is surjective (every $k$-embedding of $F$ actually arises), and (2) every fibre has the same size, namely $[K : F]_s$. [/guided] [/step] [step:Show the restriction map is surjective] Let $\sigma: F \hookrightarrow \overline{k}$ be a $k$-embedding. We show $\sigma$ extends to a $k$-embedding $K \hookrightarrow \overline{k}$. Since $K/F$ is a finite extension, write $K = F(\alpha_1, \ldots, \alpha_r)$ for algebraic elements $\alpha_1, \ldots, \alpha_r$ over $F$. We extend $\sigma$ one generator at a time. At each stage, if $\sigma_j: F(\alpha_1, \ldots, \alpha_j) \hookrightarrow \overline{k}$ has been constructed, let $m_j \in F(\alpha_1, \ldots, \alpha_j)[x]$ be the minimal polynomial of $\alpha_{j+1}$ over $F(\alpha_1, \ldots, \alpha_j)$. The image $\sigma_j(m_j) \in \overline{k}[x]$ has at least one root $\beta \in \overline{k}$ (since $\overline{k}$ is algebraically closed). By the [Structure of Simple Algebraic Extensions](/theorems/1251), the map $\sigma_{j+1}$ sending $\alpha_{j+1} \mapsto \beta$ and extending $\sigma_j$ is a well-defined field embedding $F(\alpha_1, \ldots, \alpha_{j+1}) \hookrightarrow \overline{k}$. After $r$ steps, we obtain an extension $\tau: K \hookrightarrow \overline{k}$ with $\tau|_F = \sigma$. Hence $\operatorname{res}$ is surjective. [guided] Given a $k$-embedding $\sigma: F \hookrightarrow \overline{k}$, we need to extend it to all of $K$. The idea is to adjoin the generators of $K/F$ one at a time. Write $K = F(\alpha_1, \ldots, \alpha_r)$. Set $\sigma_0 = \sigma$ and $F_0 = F$, $F_j = F(\alpha_1, \ldots, \alpha_j)$. Suppose we have extended $\sigma$ to an embedding $\sigma_j: F_j \hookrightarrow \overline{k}$. We want to extend $\sigma_j$ to $F_{j+1} = F_j(\alpha_{j+1})$. Let $m_j \in F_j[x]$ be the minimal polynomial of $\alpha_{j+1}$ over $F_j$. Apply $\sigma_j$ to the coefficients of $m_j$ to get a polynomial $\sigma_j(m_j) \in \overline{k}[x]$. Since $\overline{k}$ is algebraically closed, $\sigma_j(m_j)$ has at least one root $\beta \in \overline{k}$. By the [Structure of Simple Algebraic Extensions](/theorems/1251), $F_{j+1} \cong F_j[x]/(m_j)$, and the map $\sigma_{j+1}$ defined by $\sigma_{j+1}(\alpha_{j+1}) = \beta$ and $\sigma_{j+1}|_{F_j} = \sigma_j$ extends to a field embedding $F_{j+1} \hookrightarrow \overline{k}$. (This is well-defined because $m_j(\alpha_{j+1}) = 0$ maps to $\sigma_j(m_j)(\beta) = 0$.) Iterating $r$ times produces $\tau = \sigma_r: K \hookrightarrow \overline{k}$ with $\tau|_F = \sigma$, proving surjectivity. [/guided] [/step] [step:Show each fibre has size $[K : F]_s$] Fix $\sigma \in \operatorname{Emb}_k(F, \overline{k})$. The fibre $\operatorname{res}^{-1}(\sigma)$ consists of all $k$-embeddings $\tau: K \hookrightarrow \overline{k}$ extending $\sigma$. [claim:The fibre has cardinality $[K : F]_s$] Define a bijection \begin{align*} \Phi: \operatorname{res}^{-1}(\sigma) &\to \operatorname{Emb}_F(K, \overline{k}) \\ \tau &\mapsto \sigma^{-1} \circ \tau, \end{align*} where $\sigma^{-1}: \sigma(F) \to F$ is the inverse of $\sigma$ viewed as an isomorphism $F \xrightarrow{\sim} \sigma(F)$, and we identify $K$ as an extension of $F$. More precisely: since $\sigma: F \xrightarrow{\sim} \sigma(F) \subset \overline{k}$ is an isomorphism, we can transport the extension $K/F$ along $\sigma$. Given $\tau \in \operatorname{res}^{-1}(\sigma)$, the map $\tau: K \hookrightarrow \overline{k}$ satisfies $\tau|_F = \sigma$. We count extensions of $\sigma$ to $K$. Alternatively, and more directly: the number of extensions of $\sigma: F \hookrightarrow \overline{k}$ to an embedding $K \hookrightarrow \overline{k}$ depends only on the extension $K/F$ and not on the particular embedding $\sigma$. This is because any two $k$-embeddings $\sigma_1, \sigma_2: F \hookrightarrow \overline{k}$ are related by an automorphism $\phi \in \operatorname{Aut}(\overline{k}/k)$ (by the [Extension of Isomorphisms to Splitting Fields](/theorems/3313) applied to the normal extension $\overline{k}/k$), and post-composition with $\phi$ gives a bijection between the extensions of $\sigma_1$ and the extensions of $\sigma_2$. Taking $\sigma_1 = \operatorname{id}_F$ (the inclusion $F \hookrightarrow \overline{k}$), the number of extensions is $|\operatorname{Emb}_F(K, \overline{k})| = [K : F]_s$. [/claim] [proof] Let $\sigma_1, \sigma_2 \in \operatorname{Emb}_k(F, \overline{k})$. The algebraic closure $\overline{k}$ is a splitting field of the set of all polynomials in $k[x]$, so by the [Extension of Isomorphisms to Splitting Fields](/theorems/3313), the isomorphism $\sigma_2 \circ \sigma_1^{-1}: \sigma_1(F) \xrightarrow{\sim} \sigma_2(F)$ extends to an automorphism $\phi: \overline{k} \xrightarrow{\sim} \overline{k}$. The map $\tau \mapsto \phi \circ \tau$ sends $\operatorname{res}^{-1}(\sigma_1) \to \operatorname{res}^{-1}(\sigma_2)$ bijectively (with inverse $\tau \mapsto \phi^{-1} \circ \tau$). Hence $|\operatorname{res}^{-1}(\sigma_1)| = |\operatorname{res}^{-1}(\sigma_2)|$. For the canonical embedding $\iota: F \hookrightarrow \overline{k}$ (the inclusion), the fibre $\operatorname{res}^{-1}(\iota)$ is exactly $\operatorname{Emb}_F(K, \overline{k})$, which has cardinality $[K : F]_s$ by definition. [/proof] [guided] We need to show that for every $\sigma \in \operatorname{Emb}_k(F, \overline{k})$, the number of $k$-embeddings $\tau: K \hookrightarrow \overline{k}$ extending $\sigma$ is exactly $[K : F]_s$. Why should the fibre size be independent of $\sigma$? The key insight is that $\overline{k}$ is "large enough" that any two embeddings of $F$ into $\overline{k}$ are conjugate by an automorphism of $\overline{k}$. Concretely: given $\sigma_1, \sigma_2 \in \operatorname{Emb}_k(F, \overline{k})$, the map $\sigma_2 \circ \sigma_1^{-1}: \sigma_1(F) \to \sigma_2(F)$ is a $k$-isomorphism. By the [Extension of Isomorphisms to Splitting Fields](/theorems/3313), this extends to an automorphism $\phi \in \operatorname{Aut}(\overline{k})$. Post-composing with $\phi$ gives a bijection \begin{align*} \operatorname{res}^{-1}(\sigma_1) &\xrightarrow{\sim} \operatorname{res}^{-1}(\sigma_2), \qquad \tau \mapsto \phi \circ \tau. \end{align*} This is well-defined: if $\tau|_F = \sigma_1$, then $(\phi \circ \tau)|_F = \phi \circ \sigma_1 = \sigma_2$. The inverse is $\tau \mapsto \phi^{-1} \circ \tau$. Now we identify the common fibre size. Take $\sigma = \iota: F \hookrightarrow \overline{k}$ to be the inclusion. Then $\operatorname{res}^{-1}(\iota)$ is the set of $k$-embeddings $\tau: K \hookrightarrow \overline{k}$ with $\tau|_F = \operatorname{id}_F$, which is precisely $\operatorname{Emb}_F(K, \overline{k})$. By definition, $|\operatorname{Emb}_F(K, \overline{k})| = [K : F]_s$. [/guided] [/step] [step:Conclude the product formula and the separability criterion] Since $\operatorname{res}$ is surjective and each of the $[F : k]_s$ fibres has size $[K : F]_s$: \begin{align*} [K : k]_s = \sum_{\sigma \in \operatorname{Emb}_k(F, \overline{k})} |\operatorname{res}^{-1}(\sigma)| = [F : k]_s \cdot [K : F]_s. \end{align*} For the "in particular" statement, $K/k$ is separable iff $[K : k]_s = [K : k]$. By the tower law for degrees, $[K : k] = [K : F] \cdot [F : k]$. Since $[K : F]_s \leq [K : F]$ and $[F : k]_s \leq [F : k]$ (the separable degree never exceeds the degree), the product $[K : F]_s \cdot [F : k]_s \leq [K : F] \cdot [F : k]$, with equality if and only if both factors are equalities. Therefore $[K : k]_s = [K : k]$ if and only if $[K : F]_s = [K : F]$ and $[F : k]_s = [F : k]$, i.e., $K/k$ is separable iff both $K/F$ and $F/k$ are separable. [/step]