@misc{FIELD_14.MIZ,
      AUTHOR = {Schwarzweller, Christoph and Rowi\'{n}ska-Schwarzweller, Agnieszka},
      TITLE = {Simple Extensions},
      ADDRESS1 = {Institute of Informatics, University of Gdansk, Poland},
      ADDRESS2 = {Sopot, Poland},
      SECTION1 = {Preliminaries},
      SECTION2 = {More on Bags},
      SECTION3 = {More on Polynomials},
      SECTION4 = {On Divisibility and Polynomial GCDs},
      SECTION5 = {Formal Derivation of Polynomials and Multiplicity of Roots},
      SECTION6 = {Simple Extensions},
      DAY = {18},
      MONTH = {December},
      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 simple extensions: an extension $E$ of $F$ is simple if 
        $E is generated over $F$ by a single element of $E$, that is $E = F(a)$ 
        for some $a \in E$.
        First, we prove that a finite extension $E$ of $F$ is simple if and only 
        if there are only finitely many intermediate fields between $E$ and $F$
        \cite{Lan02}. 
        Second, we show that finite extensions of a field $F$ with characteristic 0 
        are always simple \cite{Gat11}. For this we had to prove, that irreducible 
        polynomials over $F$ have single roots only, which required extending 
        results on divisibilty and gcds of polynomials \cite{RING_4.ABS,RING_5.ABS} and 
        formal derivaton of polynomials \cite{RINGDER1.ABS}.}}

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

@BOOK{Gat11,
      AUTHOR = {Andreas Gathmann},
      TITLE = {Einf\"{u}hrung in die Algebra},
      PUBLISHER = {Lecture Notes, University of Kaiserslautern, Germany},
      YEAR = {2011}}
