<abstract xmlns="http://www.w3.org/1999/xhtml">

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 <italic>X</italic>2 − 2, <italic>X</italic>3 − 1, <italic>X</italic>2 + <italic>X</italic> + 1 and <italic>X</italic>3 − 2 over <italic>Q</italic> 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 <italic>X</italic>3 − 2 does not split over <inline-formula>
<alternatives>
<inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2022-0003_eq_001.png"></inline-graphic>
<math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"><mrow><mi>𝒬</mi><mrow><mo>(</mo><mrow><mroot><mn>2</mn><mn>3</mn></mroot></mrow><mo>)</mo></mrow></mrow></math>
<tex-math>\mathcal{Q}\left( {\root 3 \of 2 } \right)</tex-math>
</alternatives>
</inline-formula>. Because <italic>X</italic>3 − 2 obviously has a root over <inline-formula>
<alternatives>
<inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2022-0003_eq_002.png"></inline-graphic>
<math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"><mrow><mi>𝒬</mi><mrow><mo>(</mo><mrow><mroot><mn>2</mn><mn>3</mn></mroot></mrow><mo>)</mo></mrow></mrow></math>
<tex-math>\mathcal{Q}\left( {\root 3 \of 2 } \right)</tex-math>
</alternatives>
</inline-formula> this shows that the field extension <inline-formula>
<alternatives>
<inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2022-0003_eq_003.png"></inline-graphic>
<math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"><mrow><mi>𝒬</mi><mrow><mo>(</mo><mrow><mroot><mn>2</mn><mn>3</mn></mroot></mrow><mo>)</mo></mrow></mrow></math>
<tex-math>\mathcal{Q}\left( {\root 3 \of 2 } \right)</tex-math>
</alternatives>
</inline-formula> is not normal over <italic>Q</italic> [3], [4], [5] and [7].
</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 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 


𝒬(23)
\mathcal{Q}\left( {\root 3 \of 2 } \right)

. Because X3 − 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].

Splitting Fields for the Rational Polynomials X2−2, X2+X+1, X3−1, and X3−2

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

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...

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

Published Online: Dec 21, 2022

Page range: 23 - 30

Accepted: Apr 30, 2022

DOI: https://doi.org/10.2478/forma-2022-0003

Keywords
splitting fields, rational polynomials

© 2022 Christoph Schwarzweller et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Splitting Fields for the Rational Polynomials X2−2, X2+X+1, X3−1, and X3−2

Published Online: Dec 21, 2022

Page range: 23 - 30

Accepted: Apr 30, 2022

DOI: https://doi.org/10.2478/forma-2022-0003

Keywordssplitting fields, rational polynomials

© 2022 Christoph Schwarzweller et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

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

Keywords
splitting fields, rational polynomials