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

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 𝒬(23) \mathcal{Q}\left( {\root 3 \of 2 } \right) . Because X³ − 2 obviously has a root over 𝒬(23) \mathcal{Q}\left( {\root 3 \of 2 } \right) this shows that the field extension 𝒬(23) \mathcal{Q}\left( {\root 3 \of 2 } \right) is not normal over Q [3], [4], [5] and [7].