@misc{FIELD_5.MIZ,
      AUTHOR = {Schwarzweller, Christoph},
      TITLE = {Renamings and a Condition-free Formalization of {K}ronecker's Construction},
      ADDRESS1 = {Institute of Informatics, University of Gdansk, Poland},
      SECTION1 = {Preliminaries},
      SECTION2 = {Linear Polynomials},
      SECTION3 = {More on Polynom-Ring(F,p)},
      SECTION4 = {On Embedding F into F[X]/<p> and Polynom-Ring(F,p)},
      SECTION5 = {Renamings},
      SECTION6 = {Kronecker's Construction},
      DAY = {19},
      MONTH = {May},
      YEAR = {2020},
      SUMMARY = {In \cite{FIELD_1.ABS,FIELD_4.ABS,Schw18} we presented a formalization 
      of Kronecker's construction of a field extension $E$ for a field $F$ in 
      which a given polynomial $p \in F[X] \backslash F$ 
      has a root \cite{HL99,Rad89,Jac85}. A drawback of our formalization was 
      that it works only for polynomial-disjoint fields, that is for fields 
      $F$ with $F \cap F[X] = \emptyset$. 
      The main purpose of Kronecker's construction is that by induction one 
       gets a field extension of $F$ in 
      which $p$ splits into linear factors. For our formalization this means that 
      the constructed field extension $E$ again has to be polynomial-disjoint.\par
      In this article we first analyze whether our formalization can be extended 
      that way. Using the field of polynomials over $F$ with degree smaller than the 
      degree of $p$ to construct the field extension $E$ does not work: 
      In this case $E$ is polynomial-disjoint if and only if $p$ is linear. 
      Using $F[x]\backslash <p>$ one can show that for $F = \mathbb{Q} and 
      $F = \mathbb{Z}_n$ the constructed field extension $E$ is again 
      polynomial-disjoint, so that in particular algebraic number fields can 
      be handled.\par
      For the general case we then introduce renamings of sets $X$ as 
      injective functions $f$ with dom$(f) = X$ and rng$(f) \cap (X \cup Z) = \emptyset$ 
      for an arbitrary set $Z$. This, finally, allows to construct a field 
      extension $E$ of an arbitrary field $F$ in which a given polynomial 
      $p \in F[x] \backslash F$ splits into 
      linear factors. Note, however, that to prove the existence 
      of renamings we had to rely on the axiom of choice.}}

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