Separable Polynomials and Separable Extensions

We continue the formalization of field theory in Mizar [2], [3], [4]. We introduce separability of polynomials and field extensions: a polynomial is separable, if it has no multiple roots in its splitting field; an algebraic extension E of F is separable, if the minimal polynomial of each a ∈ E is separable. We prove among others that a polynomial q(X) is separable if and only if the gcd of q(X) and its (formal) derivation equals 1 – and that a irreducible polynomial q(X) is separable if and only if its derivation is not 0 – and that q(X) is separable if and only if the number of q(X)’s roots in some field extension equals the degree of q(X).

A field F is called perfect if all irreducible polynomials over F are separable, and as a consequence every algebraic extension of F is separable. Every field with characteristic 0 is perfect [13]. To also consider separability in fields with prime characteristic p we define the rings R^p = { a^p | a ∈ R} and the polynomials Xⁿ − a for a ∈ R. Then we show that a field F with prime characteristic p is separable if and only if F = F ^p and that finite fields are perfect. Finally we prove that for fields F ⊆ K ⊆ E where E is a separable extension of F both E is separable over K and K is separable over F .