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

### License

BSD License

### Topics

- Mathematics/Algebra

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

### Depends on

- Algebraic Numbers in Isabelle/HOL
- The Hermite–Lindemann–Weierstraß Transcendence Theorem
- Executable Multivariate Polynomials

### Used by

- Undecidability Results on Orienting Single Rewrite Rules
- The Schwartz-Zippel Lemma
- A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
- Solving Cubic and Quartic Equations
- Linear Recurrences

### Auto-related entries

- Continued Fractions
- Interval Arithmetic on 32-bit Words
- The Transcendence of Certain Infinite Series
- Signature-Based Gröbner Basis Algorithms
- Weight-Balanced Trees

## Cite

×

Factor_Algebraic_Polynomial-AFP

    @article{Factor_Algebraic_Polynomial-AFP,
      author  = {Manuel Eberl and René Thiemann},
      title   = {Factorization of Polynomials with Algebraic Coefficients},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Factor_Algebraic_Polynomial.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Nov 14, 2021 : Isabelle2021