On the Intersection of Fields F with F [X]
This is the third part of a four-article series containing a Mizar [3], [1], [2] formalization of Kronecker’s construction about roots of polynomials in field extensions, i.e. that for every field F and every polynomial p ∈ F [X]\F there exists a field extension E of F such that p has a root over E....
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Sciendo
2019-10-01
|
| Series: | Formalized Mathematics |
| Subjects: | |
| Online Access: | https://doi.org/10.2478/forma-2019-0021 |
| id |
doaj-22624c0d87434be2ba9ba47cebfea9c6 |
|---|---|
| record_format |
Article |
| spelling |
doaj-22624c0d87434be2ba9ba47cebfea9c62021-09-05T21:01:04ZengSciendoFormalized Mathematics1426-26301898-99342019-10-0127322322810.2478/forma-2019-0021forma-2019-0021On the Intersection of Fields F with F [X]Schwarzweller Christoph0Institute of Informatics, University of GdańskPolandThis is the third part of a four-article series containing a Mizar [3], [1], [2] formalization of Kronecker’s construction about roots of polynomials in field extensions, i.e. that for every field F and every polynomial p ∈ F [X]\F there exists a field extension E of F such that p has a root over E. The formalization follows Kronecker’s classical proof using F [X]/<p> as the desired field extension E [6], [4], [5].https://doi.org/10.2478/forma-2019-0021roots of polynomialsfield extensionskronecker’s construction12e0512f0568t9903b35 |
| collection |
DOAJ |
| language |
English |
| format |
Article |
| sources |
DOAJ |
| author |
Schwarzweller Christoph |
| spellingShingle |
Schwarzweller Christoph On the Intersection of Fields F with F [X] Formalized Mathematics roots of polynomials field extensions kronecker’s construction 12e05 12f05 68t99 03b35 |
| author_facet |
Schwarzweller Christoph |
| author_sort |
Schwarzweller Christoph |
| title |
On the Intersection of Fields F with F [X] |
| title_short |
On the Intersection of Fields F with F [X] |
| title_full |
On the Intersection of Fields F with F [X] |
| title_fullStr |
On the Intersection of Fields F with F [X] |
| title_full_unstemmed |
On the Intersection of Fields F with F [X] |
| title_sort |
on the intersection of fields f with f [x] |
| publisher |
Sciendo |
| series |
Formalized Mathematics |
| issn |
1426-2630 1898-9934 |
| publishDate |
2019-10-01 |
| description |
This is the third part of a four-article series containing a Mizar [3], [1], [2] formalization of Kronecker’s construction about roots of polynomials in field extensions, i.e. that for every field F and every polynomial p ∈ F [X]\F there exists a field extension E of F such that p has a root over E. The formalization follows Kronecker’s classical proof using F [X]/<p> as the desired field extension E [6], [4], [5]. |
| topic |
roots of polynomials field extensions kronecker’s construction 12e05 12f05 68t99 03b35 |
| url |
https://doi.org/10.2478/forma-2019-0021 |
| work_keys_str_mv |
AT schwarzwellerchristoph ontheintersectionoffieldsfwithfx |
| _version_ |
1717781682843549696 |