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

<p>In this article we further develop field theory [6], [7], [12] in Mizar [1], [2], [3]: we deal with quadratic polynomials and quadratic extensions [5], [4]. First we introduce quadratic polynomials, their discriminants and prove the midnight formula. Then we show that - in case the discriminant of <italic>p</italic> being non square - adjoining a root of <italic>p</italic>’s discriminant results in a splitting field of <italic>p</italic>. Finally we prove that these are the only field extensions of degree 2, e.g. that an extension <italic>E</italic> of <italic>F</italic> is quadratic if and only if there is a non square Element <italic>a</italic> ∈ <italic>F</italic> such that <italic>E</italic> and  (<inline-formula>
<alternatives>
<inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2021-0021_eq_001.png"></inline-graphic>
<math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"><mrow><mi>F</mi><msqrt><mi>a</mi></msqrt></mrow></math>
<tex-math>F\sqrt a</tex-math>
</alternatives>
</inline-formula>) are isomorphic over <italic>F</italic>.</p>
</abstract>

In this article we further develop field theory [6], [7], [12] in Mizar [1], [2], [3]: we deal with quadratic polynomials and quadratic extensions [5], [4]. First we introduce quadratic polynomials, their discriminants and prove the midnight formula. Then we show that - in case the discriminant of p being non square - adjoining a root of p’s discriminant results in a splitting field of p. Finally we prove that these are the only field extensions of degree 2, e.g. that an extension E of F is quadratic if and only if there is a non square Element a ∈ F such that E and  (


Fa
F\sqrt a

) are isomorphic over F.

Quadratic Extensions

Formalized Mathematics

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

{"article-title":"Quadratic Extensions"}

In this article we further develop field theory [6], [7], [12] in Mizar [1], [2], [3]: we deal with quadratic polynomials and quadratic extensions [5], [4]....

Quadratic Extensions

Publicado en línea: 09 jul 2022

Páginas: 229 - 240

Aceptado: 30 nov 2021

DOI: https://doi.org/10.2478/forma-2021-0021

Palabras clave
field extensions, quadratic polynomials, quadratic extensions

© 2022 Christoph Schwarzweller et al., published by Sciendo

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

Quadratic Extensions

Publicado en línea: 09 jul 2022

Páginas: 229 - 240

Aceptado: 30 nov 2021

DOI: https://doi.org/10.2478/forma-2021-0021

Palabras clavefield extensions, quadratic polynomials, quadratic extensions

© 2022 Christoph Schwarzweller et al., published by Sciendo

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

Palabras clave
field extensions, quadratic polynomials, quadratic extensions