@misc{FIELD_8.MIZ,      
      AUTHOR = {Schwarzweller, Christoph},
      TITLE = {Splitting Fields},
      ADDRESS1 = {Institute of Informatics, University of Gdansk, Poland},
      SECTION1 = {Preliminaries},
      SECTION2 = {More on Polynomials},
      SECTION3 = {More on Products of Linear Polynomials},
      SECTION4 = {Existence of Splitting Fields},
      SECTION5 = {Fixing and Extending Automorphisms},
      SECTION6 = {Some More Preliminaries},
      SECTION7 = {Uniqueness of Splitting Fields},
      DAY = {30},
      MONTH = {June},
      YEAR = {2021},
      SUMMARY = {In this article we further develop field theory in 
        Mizar \cite{Mizar-State-2015,BancerekJAR:2018}:
        We prove existence and uniqueness of splitting fields.
        We define the splitting field of a polynomial $p \in F[X]$ as the smallest
        field extension $E$ of $F$, in which $p$ splits into linear factors.
        From this follows, that $E = F(A)$, where $A$ is the set of $p$'s roots.
        Splitting field are unique, however, only with respect to isomorphisms;
        to be more precise with respect to $F$-isomorphims.
        We prove that two splitting fields are $F$-isomorphic using the well-known
        technique of extending isomorphisms from $F_1 \longrightarrow F_2$ to 
        $F_1(a) \longrightarrow F_2(b)$ for $a$,$b$ being $F1$-algebraic and 
        $F2$-algebraic, respectively \cite{Rad89,Lan02}.}}

@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}}

