Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/10843
Tytuł: | Ring and Field Adjunctions, Algebraic Elements and Minimal Polynomials |
Autorzy: | Schwarzweller, Christoph |
Słowa kluczowe: | ring and field adjunctions algebraic elements and minimal polynomials |
Data wydania: | 2020 |
Data dodania: | 5-maj-2021 |
Wydawca: | DeGruyter Open |
Źródło: | Formalized Mathematics, Volume 28, Issue 3, Pages 251-261 |
Abstrakt: | 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 . |
Afiliacja: | Institute of Informatics, University of Gdansk, Poland |
URI: | http://hdl.handle.net/11320/10843 |
DOI: | 10.2478/forma-2020-0022 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
metadata.dc.identifier.orcid: | 0000-0001-9587-8737 |
Typ Dokumentu: | Article |
metadata.dc.rights.uri: | https://creativecommons.org/licenses/by-sa/3.0/ |
Właściciel praw: | © 2020 University of Białymstoku; CC-BY-SA License ver. 3.0 or later; |
Występuje w kolekcji(ach): | Formalized Mathematics, 2020, Volume 28, Issue 3 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
10.2478_forma-2020-0022.pdf | 291,06 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL