Email Gateway (Nov 14 2021 at 03:49): Email Gateway (Nov 14 2021 at 03:49):From: Gerwin Klein <kleing@unsw.edu.au>
Factorization of Polynomials with Algebraic Coefficients
by Manuel Eberl and René Thiemann
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.
https://www.isa-afp.org/entries/Factor_Algebraic_Polynomial.html
Enjoy!
Gerwin
Last updated: Jul 15 2022 at 23:21 UTC