**This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.**

### Abstract

Based on existing libraries for matrices, factorization of rational polynomials, and Sturm's theorem, we formalized algebraic numbers in Isabelle/HOL. Our development serves as an implementation for real and complex numbers, and it admits to compute roots and completely factorize real and complex polynomials, provided that all coefficients are rational numbers. Moreover, we provide two implementations to display algebraic numbers, an injective and expensive one, or a faster but approximative version.

BSD LicenseTo this end, we mechanized several results on resultants, which also required us to prove that polynomials over a unique factorization domain form again a unique factorization domain.

### Change history

#### April 16, 2017

Use certified Berlekamp-Zassenhaus factorization, use subresultant algorithm for computing resultants, improved bisection algorithm

#### January 29, 2016

Split off Polynomial Interpolation and Polynomial Factorization### Topics

### Theories of Algebraic_Numbers

- Algebraic_Numbers_Prelim
- Bivariate_Polynomials
- Resultant
- Algebraic_Numbers
- Sturm_Rat
- Factors_of_Int_Poly
- Min_Int_Poly
- Algebraic_Numbers_Pre_Impl
- Cauchy_Root_Bound
- Real_Algebraic_Numbers
- Real_Roots
- Complex_Roots_Real_Poly
- Compare_Complex
- Interval_Arithmetic
- Complex_Algebraic_Numbers
- Show_Real_Alg
- Show_Real_Approx
- Show_Real_Precise
- Algebraic_Number_Tests
- Algebraic_Numbers_External_Code