Renamings and a Condition-free Formalization of Kronecker’s Construction
In [7], [9], [10] we presented a formalization of Kronecker’s construction of a field extension E for a field F in which a given polynomial p ∈ F [X]\F has a root [5], [6], [3]. A drawback of our formalization was that it works only for polynomial-disjoint fields, that is for fields F with F ∩ F [X]...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Sciendo
2020-07-01
|
| Series: | Formalized Mathematics |
| Subjects: | |
| Online Access: | https://doi.org/10.2478/forma-2020-0012 |