### 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.

BSD License### Topics

### Theories of Factor_Algebraic_Polynomial

- Poly_Connection
- MPoly_Divide
- MPoly_Divide_Code
- MPoly_Container
- Multivariate_Resultant
- Is_Int_To_Int
- Roots_of_Algebraic_Poly
- Roots_of_Algebraic_Poly_Impl
- Roots_via_IA
- Roots_of_Real_Complex_Poly
- Factor_Complex_Poly
- Factor_Real_Poly