Separable Polynomials and Separable Extensions

Summary 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 n − 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 .