Ring and Field Adjunctions, Algebraic Elements and Minimal Polynomials
Christoph Schwarzweller · Formalized Mathematics · 2020
Summary In [6], [7] we presented a formalization of Kronecker’s construction of a field extension of a field F in which a given polynomial p ∈ F [ X ] \F has a root [4], [5], [3]. 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 . In this article we start the Mizar formalization [1], [2] 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 , . . ., a n− 1 , where n is the degree of the minimal polynomial of a over F .