@misc{FIELD_7.MIZ,
      AUTHOR = {Schwarzweller, Christoph and 
          Rowin\'{n}ska-Schwarzweller, Agnieszka},
      TITLE = {Algebraic Extensions},
      ADDRESS1 = {Institute of Informatics, University of Gdansk, Poland},
      ADDRESS2 = {Sopot, Poland},
      SECTION1 = {Preliminaries},
      SECTION2 = {More on Finite Extensions},
      SECTION3 = {Algebraic Extensions},
      SECTION4 = {The Field of Algebraic Elements},
      DAY = {30},
      MONTH = {March},
      YEAR = {2021},
      SUMMARY = {In this article we further develop field theory in
     Mizar \cite{Mizar-State-2015,BancerekJAR:2018,GrabKornSchwarz:2016}
     towards splitting fields.
     We deal with algebraic extensions \cite{Jac85,Lan02}:
     A field extension $E$ of a field $F$ is
     algebraic, if every element of $E$ is algebraic over $F$.
     We prove amongst others that finite
     extensions are algebraic and that field extensions generated by
     a finite set of algebraic elements are finite. From this
     immediately follows that field extensions generated by roots
     of a polynomial over $F$ are both finite and algebraic.
     We also define the field of algebraic
     elements of $E$ over $F$ and show that this field is an
     intermediate field of $E|F.$}}

@BOOK{HL99,
      AUTHOR = {H. L\"{u}neburg},
      TITLE = {Gruppen, Ringe, K\"{o}rper: Die grundlegenden Strukturen der Algebra},
      PUBLISHER = {Oldenbourg Verlag},
      YEAR = {1990}}

@BOOK{Rad89,
      AUTHOR = {Knut Radbruch},
      TITLE = {Algebra I},
      PUBLISHER = {Lecture Notes, University of Kaiserslautern, Germany},
      YEAR = {1991}}

@BOOK{Lan02,
      AUTHOR = {Serge Lang},
      TITLE = {Algebra, {R}evised {T}hird {E}dition},
      PUBLISHER = {Springer Verlag},
      YEAR = {2002}}

@BOOK{Jac85,
      AUTHOR = {Nathan Jacobson},
      TITLE = {Basic Algebra I},
      PUBLISHER = {Dover Books on Mathematics},
      YEAR = {1985}}
