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

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

### License

BSD License

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

- Mathematics/Algebra

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

### Depends on

- The Factorization Algorithm of Berlekamp and Zassenhaus
- Sturm’s Theorem

### Used by

- A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
- Factorization of Polynomials with Algebraic Coefficients
- Solving Cubic and Quartic Equations
- The BKR Decision Procedure for Univariate Real Arithmetic
- The Hermite–Lindemann–Weierstraß Transcendence Theorem
- A verified LLL algorithm
- Linear Recurrences

### Auto-related entries

- Combinatorial Enumeration Algorithms
- Factorization of Polynomials with Algebraic Coefficients
- The Hermite–Lindemann–Weierstraß Transcendence Theorem
- The Transcendence of Certain Infinite Series

## Cite

×

Algebraic_Numbers-AFP

    @article{Algebraic_Numbers-AFP,
      author  = {René Thiemann and Akihisa Yamada and Sebastiaan J. C. Joosten},
      title   = {Algebraic Numbers in Isabelle/HOL},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2015},
      note    = {\url{https://isa-afp.org/entries/Algebraic_Numbers.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
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- Dec 22, 2015 : Isabelle2015