Algebraic Numbers in Isabelle/HOL.
René Thiemann, Akihisa Yamada · 2015
We formalize algebraic numbers in Isabelle/HOL, based on existing libraries for matrices and Sturm’s theorem. Our development serves as a verified implementation for real and complex numbers, and it admits to compute roots and completely factor 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, and a faster but approximative version.