Factorization of Polynomials with Algebraic Coefficients


Title: Factorization of Polynomials with Algebraic Coefficients
Authors: Manuel Eberl and René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
Submission date: 2021-11-08
Abstract: 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.
  author  = {Manuel Eberl and René Thiemann},
  title   = {Factorization of Polynomials with Algebraic Coefficients},
  journal = {Archive of Formal Proofs},
  month   = nov,
  year    = 2021,
  note    = {\url{https://isa-afp.org/entries/Factor_Algebraic_Polynomial.html},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Algebraic_Numbers, Hermite_Lindemann, Polynomials
Used by: Cubic_Quartic_Equations
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.