Repeated roots in extension fields and separable polynomials

Let $F$ be a field, let $E$ be an extension field in which $F$ is a subfield (Subfield: a subring of a field closed under inverses of its nonzero elements, and therefore a field with the restricted operations), and let $0\ne f\in F[x]$. The coefficient inclusion induces a homomorphism $F[x]\to E[x]$ by the universal property (Universal property of $R[x]$: a coefficient homomorphism and the image of $x$ determine a unique ring homomorphism).

An element $a\in E$ is a repeated root of $f$ in $E$ when $(x-a)^2$ divides the image of $f$ in $E[x]$. It is a root in the ordinary sense of Evaluation and roots of a polynomial in a commutative target ring, and Factor theorem over a commutative ring identifies divisibility by $x-a$ with vanishing at $a$.

The polynomial $f$ is separable over $F$ when it has no repeated root in any extension field of $F$. A nonzero constant polynomial is therefore separable. The zero polynomial is not called separable under this convention.