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