Splitting Fields for the Rational Polynomials X 2 −2, X 2 +X+1, X 3 −1, and X 3 −2
Christoph Schwarzweller, Sara Burgoa · Formalized Mathematics · 2022
Summary 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 − 2, X 3 − 1, X 2 + X + 1 and X 3 − 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 3 − 2 does not split over 𝒬 ( 2 3 ) \mathcal{Q}\left( {\root 3 \of 2 } \right) . Because X 3 − 2 obviously has a root over 𝒬 ( 2 3 ) \mathcal{Q}\left( {\root 3 \of 2 } \right) this shows that the field extension 𝒬 ( 2 3 ) \mathcal{Q}\left( {\root 3 \of 2 } \right) is not normal over Q [3], [4], [5] and [7].