Let $E/K$ be an algebraic extension of fields and denote by $E_s$ the separable closure of $K$ in $E$, i.e. the set of all elements of $E$ that are separable over $K$ (which can be shown is a (separable) subfield of $E$).
I would like to show that the implication
$\left[E:K\right]_s < \infty \implies \left[E_s:K\right] < \infty$
holds, where $\left[E:K\right]_s$ denotes the separable degree of $E/K$ and $\left[E_s:K\right]$ the 'ordinary' degree of $E_s/K$.
In the textbook I am learning with, it is said that one could use the Primitive Element Theorem to do this, but I would also be fine with any other approach, as long as it's not getting too fancy and staying in the realm of 'common' textbook theorems known when dealing with separable extensions (and I didn't see how the Primitive Element Theorem would help).
This is not my focus (I want to write a Bachelor's thesis about polynomial factorizing elements of $\mathbb{Z}[X]$), but I'm in the process of reading into commutative algebra after about 1.5 years break from it.
My idea was something like assuming $\left[E_s:K\right] < \infty$ and $\left[E_s:K\right] = \infty$ to construct infinitely many $K$-homomorphisms $E_s/K \longrightarrow C/K$, where $C$ is some algebraic closure of $E_s$, which would then contradict $\left[E_s:K\right]_s = \left[E_s:K\right] < \infty$. Of course, an infinite basis would yield infinitely many $K$-vector space homomorphisms, but getting (infinitely many) ring morphisms seems to by an entirely different ting (unsurprisingly so...).
Thought of using something like
Given two roots of the minimal polynomial of one of the infinitely many elements of a $K$-basis of $E_s/K$, there is a $K$-morphism $E_s/K \longrightarrow C/K$ that sends one to the other.
but this didn't seem very fruitful. I admit I haven't spent hours on this, I just didn't get very far and should focus on moving on, while still getting an answer on the 'howto' along the road would be really nice.
Suppose that $[E:k]_s = n < \infty$. Then, for every $\alpha \in E_s$ we have that $[k(\alpha):k] \leq n$. So, the set $$\mathcal{A} = \{\, [k(\alpha):k] \mid \alpha \in E_s \,\} \subset \Bbb{N}$$ is bounded above by $n$. Let $m = \max(\mathcal{A})$ and let $\alpha_0 \in E_s$ be an element for which the maximum is attained.
We claim that $E_s = k(\alpha_0)$. Since $k(\alpha_0) \subset E_s$, it suffices to show that $E_s \subset k(\alpha_0)$. So, let $\beta \in E_s$ and consider $k(\alpha_0,\beta) \subset E_s$. Since $k(\alpha_0,\beta)$ is separable over $k$, by the primitive element theorem there exists $\gamma \in k(\alpha_0,\beta)$ such that $k(\alpha_0,\beta) = k(\gamma)$.
Since $k(\alpha_0) \subset k(\gamma)$, $[k(\gamma):k] \geq [k(\alpha_0):k] = m$. But, $m$ was chosen to be $\max(\mathcal{A})$, so $[k(\gamma):k] \leq m$. Hence, $[k(\gamma):k] = m$. Thus, $k(\alpha_0)$ is a subfield of $k(\gamma)$ with both having the same (finite) degree over $k$. Hence, $k(\alpha_0) = k(\gamma)$ and so, $\beta \in k(\alpha_0)$. Hence, $E_s \subset k(\alpha_0)$.
Hence, $[E_s : k] = m < \infty$.
In fact, not only is $[E_s:k] = m \leq n$, but in fact $[E_s:k]=n$. By Proposition V.6.6 in Lang's Algebra, $E/E_s$ is purely inseparable, so $[E:E_s] = 1$. So, by the tower law of separable degree, we get $$ \begin{align} [E:k]_s &= [E:E_s]_s \cdot [E_s:k]_s\\ &= 1 \cdot [E_s:k], \end{align} $$ since $E_s \supset k$ being a finite separable extension implies that $[E_s:k]_s = [E_s:k]$. Thus, $$n = [E:k]_s = [E_s:k] = m.$$