@misc{FIELD_13.MIZ,
      AUTHOR = {Schwarzweller, Christoph},
      TITLE = {Normal Extensions},
      ADDRESS1 = {Institute of Informatics, University of Gdansk, Poland},
      DAY = {30},
      MONTH = {June},
      YEAR = {2023},
      SUMMARY = {In this article we continue the formalization of field theory 
      in Mizar \cite{Mizar-State-2015,BancerekJAR:2018,GrabKornSchwarz:2016}.
      We introduce normal extensions: an (algebraic) extension 
      $E$ of $F$ is normal if every polynomial of $F$ that has a root in 
      $E$ already splits in $E$.
      We proved characterizations (for finite extensions) by minimal 
     polynomials, splitting fields, and fixing monomorphisms \cite{Rad91,Lan02}. 
     This required extending results from \cite{FIELD_6.ABS} and \cite{FIELD_8.ABS}, 
      in particular that $F[T] = \{ p(a_1, \ldots a_n) | p \in F[X],\ a_i \in T \}$ 
      and $F(T) = F[T]$ for finite (algebraic) $T \subseteq E$.
      We also provided the counter example that ${\cal Q}(\sqrt[3]{2})$
      is not normal over ${\cal Q}$ (compare \cite{FIELD_10.ABS}).}}

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

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