<abstract xmlns="http://www.w3.org/1999/xhtml">In [6], [7] we presented a formalization of Kronecker’s construction of a field extension of a field <italic>F</italic> in which a given polynomial <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>]<italic>\F</italic> has a root [4], [5], [3]. As a consequence for every field <italic>F</italic> and every polynomial there exists a field extension <italic>E</italic> of <italic>F</italic> in which <italic>p</italic> splits into linear factors. It is well-known that one gets the smallest such field extension – the splitting field of <italic>p</italic> – by adjoining the roots of <italic>p</italic> to <italic>F</italic>.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 <italic>a</italic> over <italic>F</italic> a basis of the vector space <italic>F</italic> (<italic>a</italic>) over <italic>F</italic> is given by <italic>a</italic>0<italic>, . . ., an−</italic>1, where <italic>n</italic> is the degree of the minimal polynomial of <italic>a</italic> over <italic>F</italic> .</abstract>

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 a0, . . ., an−1, where n is the degree of the minimal polynomial of a over F .

Ring and Field Adjunctions, Algebraic Elements and Minimal Polynomials

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

{"article-title":"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],...

Ring and Field Adjunctions, Algebraic Elements and Minimal Polynomials

Data publikacji: 06 kwi 2021

Zakres stron: 251 - 261

Przyjęty: 25 wrz 2020

DOI: https://doi.org/10.2478/forma-2020-0022

Słowa kluczowe
ring and field adjunctions, algebraic elements and minimal polynomials

© 2020 Christoph Schwarzweller, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Ring and Field Adjunctions, Algebraic Elements and Minimal Polynomials

Data publikacji: 06 kwi 2021

Zakres stron: 251 - 261

Przyjęty: 25 wrz 2020

DOI: https://doi.org/10.2478/forma-2020-0022

Słowa kluczowering and field adjunctions, algebraic elements and minimal polynomials

© 2020 Christoph Schwarzweller, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Słowa kluczowe
ring and field adjunctions, algebraic elements and minimal polynomials