@misc{REALALG3.MIZ,
      AUTHOR = {Schwarzweller, Christoph},
      TITLE = {Extensions of Orderings},
      ADDRESS1 = {Institute of Informatics, University of Gdansk, Poland},
      SECTION1 = {Preliminaries},
      SECTION2 = {Some Properties of Polynomials},
      SECTION3 = {More on the fields $F(a)$},
      SECTION4 = {Extensions of orderings},
      DAY = {18},
      MONTH = {December},
      YEAR = {2023},
      SUMMARY = {In this article we extend the algebraic theory of ordered fields
                 \cite{Pre84,Rad91}
                 in Mizar \cite{Mizar-State-2015,BancerekJAR:2018,GrabKornSchwarz:2016}.
                 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 suffiecient conditions for $P$ being 
                 extendable to $E$, in particular that $P$ extends to $E$ if and only if the 
                 set $QS \ E := \{ a * b^2 \ | \ a \in P, b \in E \}$ is a preordering of $E$ 
                 -- or equivalently if and only if $ -1 \notin QS \ E$.\\
                 Then we show that $P$ extends to $F(\sqrt{a})$ if and only if $\a \in P$ and
                 finally that every ordering $P$ of $F$ extends to $E$ if the degree of $E$ 
                 over $F$ is odd.    }}

@BOOK{Pre84,
      AUTHOR = {Alexander Prestel},
      TITLE = {Lectures on Formally Real Fields},
      PUBLISHER = {Springer Verlag},
      YEAR = {1984}}

@BOOK{Rad91,
      AUTHOR = {Knut Radbruch},
      TITLE = {Geordnete K\"{o}rper},
      PUBLISHER = {Lecture Notes, University of Kaiserslautern, Germany},
      YEAR = {1991}}
