Factorization of Polynomials with Algebraic Coefficients (Q7361482)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Factor_Algebraic_Polynomial
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Factorization of Polynomials with Algebraic Coefficients |
AFP entry Factor_Algebraic_Polynomial |
Statements
8 November 2021
0 references
Manuel Eberl
0 references
René Thiemann
0 references
Factorization of Polynomials with Algebraic Coefficients (English)
0 references
The AFP already contains a verified implementation of algebraic numbers. However, it is has a severe limitation in its factorization algorithm of real and complex polynomials: the factorization is only guaranteed to succeed if the coefficients of the polynomial are rational numbers. In this work, we verify an algorithm to factor all real and complex polynomials whose coefficients are algebraic. The existence of such an algorithm proves in a constructive way that the set of complex algebraic numbers is algebraically closed. Internally, the algorithm is based on resultants of multivariate polynomials and an approximation algorithm using interval arithmetic.
0 references
