Algebraic Numbers in Isabelle/HOL (Q7361619)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Algebraic_Numbers
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Algebraic Numbers in Isabelle/HOL |
AFP entry Algebraic_Numbers |
Statements
René Thiemann
0 references
Akihisa Yamada
0 references
Sebastiaan J. C. Joosten
0 references
Manuel Eberl
0 references
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.
0 references
22 December 2015
0 references
Algebraic Numbers in Isabelle/HOL (English)
0 references
