Separable Polynomials and Separable Extensions

Abstract

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). Afield 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 Rp = { ap | a ∈ R} and the polynomials Xn −a for a ∈ R. Then we show that a field F with prime characteristic p is separable if and only if F = Fp 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.