@misc{FIELD_6.MIZ,
      AUTHOR = {Schwarzweller, Christoph},
      TITLE = {Ring and Field Adjunctions, Algebraic Elements and Minimal Polynomials},
      ADDRESS1 = {Institute of Informatics, University of Gdansk, Poland},
     SECTION1 = {Preliminaries},
     SECTION2 = {On Subrings and Subfields},
     SECTION3 = {Ring and Field Adjunctions},
     SECTION4 = {Algebraic Elements},
     SECTION5 = {On Linear Combinations and Polynomials},
     SECTION6 = {Minimal Polynomials},
     SECTION7 = {The Basis of Vector Space F(a)}
      DAY = {25},
      MONTH = {October},
      YEAR = {2020},
      SUMMARY = {In \cite{FIELD_5,Schw18} we presented a formalization of Kronecker's construction of
                 a field extension of a field $F$ in which a given polynomial $p \in F[X] \backslash F$ 
                 has a root \cite{HL99,Rad89,Jac85}. As a consequence for every field $F$ and every
                 polynomial there exists a field extension $E$ of $F$ in which $p$ splits into linear
                 factors. It is well-known that one gets the smallest such field extension -- the splitting field 
                 of $p$ -- by adjoining the roots of $p$ to $F$.\par
                 In this article we start the Mizar formalization towards splitting fields: We define
                 ring and field adjunctions, algebraic elements and minimal polynomials and prove a
                 number of facts necessary to develop the theory of splitting fields, in particular
                 that for an algebraic element $a$ over $F$ a basis of the vector space $F(a)$ over
                 $F$ is given by $a^0, \ldots a^{n-1}$, where $n$ is the degree of the minimal polynomial
                 of $a$ over $F$.}}

@inproceedings{Schw18,
	author={Christoph Schwarzweller},
	pages={67--72},
	title={Representation Matters: An Unexpected Property of Polynomial Rings and its Consequences for Formalizing Abstract Field Theory},
	booktitle={Proceedings of the 2018 Federated Conference on Computer Science and Information Systems},
	year={2018},
	editor={M. Ganzha and L. Maciaszek and M. Paprzycki},
	publisher={IEEE},
	doi={10.15439/2018F88},
	url={http://dx.doi.org/10.15439/2018F88},
	volume={15},
	series={Annals of Computer Science and Information Systems}}

@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{Jac85,
      AUTHOR = {Nathan Jacobson},
      TITLE = {Basic Algebra I},
      PUBLISHER = {Dover Books on Mathematics},
      YEAR = {1985}}

