Email Gateway (Aug 22 2022 at 12:05): Email Gateway (Aug 22 2022 at 12:05):From: Lawrence Paulson <lp15@cam.ac.uk>
Today we have an embarrassment of riches in the form of a third, and substantial, AFP entry. Abstract:
"Based on existing libraries for matrices 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 rational, 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.”
The full entry is here:
http://afp.sourceforge.net/entries/Algebraic_Numbers.shtml
Once again, many thanks to the authors!
Larry Paulson
Last updated: Apr 25 2024 at 08:20 UTC