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

<p>In this article we extend the algebraic theory of ordered fields [<xref ref-type="bibr" rid="j_forma-2023-0027_ref_006">6</xref>], [<xref ref-type="bibr" rid="j_forma-2023-0027_ref_008">8</xref>] in Mizar. We introduce extensions of orderings: if <italic>E</italic> is a field extension of <italic>F</italic>, then an ordering <italic>P</italic> of <italic>F</italic> extends to <italic>E</italic>, if there exists an ordering <italic>O</italic> of <italic>E</italic> containing <italic>P</italic>. We first prove some necessary and su cient conditions for <italic>P</italic> being extendable to <italic>E</italic>, in particular that <italic>P</italic> extends to <italic>E</italic> if and only if the set 
<inline-formula>
<alternatives>
<inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2023-0027_ieq_001.png"></inline-graphic>
<math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mrow><mi>Q</mi><mi>S</mi><mi> </mi><mi> </mi><mi>E</mi><mo>:</mo><mo>=</mo><mrow><mo>{</mo> <mrow><mo>∑</mo> <mrow><mi>a</mi><mo>*</mo><msup><mrow><mi>b</mi></mrow><mn>2</mn></msup><mo>|</mo><mi>a</mi><mo>∈</mo><mi>P</mi><mo>,</mo><mi> </mi><mi> </mi><mi>b</mi><mo>∈</mo><mi>E</mi></mrow></mrow> <mo>}</mo></mrow></mrow></math>
<tex-math>QS\,\,E: = \left\{ {\sum {a*{b^2}|a \in P,\,\,b \in E} } \right\}</tex-math>
</alternatives>
</inline-formula>
 is a preordering of <italic>E</italic> – or equivalently if and only if −1 <italic>/</italic> ∉ <italic>QS E</italic>. Then we show for non-square <italic>a</italic> ∈ <italic>F</italic> that <italic>P</italic> extends to 
<inline-formula>
<alternatives>
<inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2023-0027_ieq_002.png"></inline-graphic>
<math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mrow><mi>F</mi><mrow><mo>(</mo><mrow><msqrt><mi>a</mi></msqrt></mrow><mo>)</mo></mrow></mrow></math>
<tex-math>F\left( {\sqrt a } \right)</tex-math>
</alternatives>
</inline-formula>
 if and only if <italic>P</italic> and finally that every ordering <italic>P</italic> of <italic>F</italic> extends to <italic>E</italic> if the degree of <italic>E</italic> over <italic>F</italic> is odd.</p>
</abstract>

In this article we extend the algebraic theory of ordered fields [6], [8] in Mizar. We introduce extensions of orderings: if E is a field extension of F, then an ordering P of F extends to E, if there exists an ordering O of E containing P. We first prove some necessary and su cient conditions for P being extendable to E, in particular that P extends to E if and only if the set 



QS  E:={ ∑ a*b2|a∈P,  b∈E }
QS\,\,E: = \left\{ {\sum {a*{b^2}|a \in P,\,\,b \in E} } \right\}


 is a preordering of E – or equivalently if and only if −1 / ∉ QS E. Then we show for non-square a ∈ F that P extends to 



F(a)
F\left( {\sqrt a } \right)


 if and only if P and finally that every ordering P of F extends to E if the degree of E over F is odd.

Extensions of Orderings

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

{"article-title":"Extensions of Orderings"}

In this article we extend the algebraic theory of ordered fields [6], [8] in Mizar. We introduce extensions of orderings: if E is a field extension of F, then...

Extensions of Orderings

Data publikacji: 31 gru 2023

Zakres stron: 341 - 352

Przyjęty: 18 gru 2023

DOI: https://doi.org/10.2478/forma-2023-0027

Słowa kluczowe
ordered fields, quadratic extensions, extensions of odd degree

© 2023 Christoph Schwarzweller, published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Extensions of Orderings

Data publikacji: 31 gru 2023

Zakres stron: 341 - 352

Przyjęty: 18 gru 2023

DOI: https://doi.org/10.2478/forma-2023-0027

Słowa kluczoweordered fields, quadratic extensions, extensions of odd degree

© 2023 Christoph Schwarzweller, published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Słowa kluczowe
ordered fields, quadratic extensions, extensions of odd degree