
Algebraic
Numbers
in
Isabelle/HOL
Title: 
Algebraic Numbers in Isabelle/HOL 
Authors:

RenĂ© Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at),
Akihisa Yamada (akihisa /dot/ yamada /at/ aist /dot/ go /dot/ jp) and
Sebastiaan Joosten

Contributor:

Manuel Eberl

Submission date: 
20151222 
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.

Change history: 
[20160129]: Split off Polynomial Interpolation and Polynomial Factorization
[20170416]: Use certified BerlekampZassenhaus factorization, use subresultant algorithm for computing resultants, improved bisection algorithm 
BibTeX: 
@article{Algebraic_NumbersAFP,
author = {RenĂ© Thiemann and Akihisa Yamada and Sebastiaan Joosten},
title = {Algebraic Numbers in Isabelle/HOL},
journal = {Archive of Formal Proofs},
month = dec,
year = 2015,
note = {\url{https://isaafp.org/entries/Algebraic_Numbers.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
Berlekamp_Zassenhaus, Sturm_Sequences 
Used by: 
BenOr_Kozen_Reif, Cubic_Quartic_Equations, Factor_Algebraic_Polynomial, Hermite_Lindemann, LLL_Basis_Reduction 
