Simple Extensions

In this article we continue the formalization of field theory in Mizar. We introduce simple extensions: an extension E of F is simple if E is generated over F by a single element of E, that is E = F (a) for some a ∈ E. First, we prove that a finite extension E of F is simple if and only if there are only finitely many intermediate fields between E and F [7]. Second, we show that finite extensions of a field F with characteristic 0 are always simple [1]. For this we had to prove, that irreducible polynomials over F have single roots only, which required extending results on divisibility and gcds of polynomials [14], [13] and formal derivation of polynomials [15].