Splitting Fields for the Rational Polynomials X²−2, X²+X+1, X³−1, and X³−2

Abstract

In [11] the existence (and uniqueness) of splitting fields has been formalized. In this article we apply this result by providing splitting fields for the polynomials X² − 2, X³ − 1, X² + X + 1 and X³ − 2 over Q using the Mizar [2], [1] formalism. We also compute the degrees and bases for these splitting fields, which requires some additional registrations to adopt types properly. The main result, however, is that the polynomial X³ − 2 does not split over Q(∛2). Because X³ − 2 obviously has a root over Q(∛2), this shows that the field extension Q(∛2) is not normal over Q [3], [4], [5] and [7].