Ring and Field Adjunctions, Algebraic Elements and Minimal Polynomials

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⁰, . . ., aⁿ⁻¹, where n is the degree of the minimal polynomial of a over F .