Sciweavers

AFP
2015
Springer

Descartes' Rule of Signs

7 years 11 months ago
Descartes' Rule of Signs
In this work, we formally proved Descartes Rule of Signs, which relates the number of positive real roots of a polynomial with the number of sign changes in its coefficient list. Our proof follows the simple inductive proof given by Arthan [1], which was also used by John Harrison in his HOL Light formalisation. We proved most of the lemmas for arbitrary linearly-ordered integrity domains (e.g. integers, rationals, reals); the main result, however, requires the intermediate value theorem and was therefore only proven for real polynomials. Contents 1 Sign changes and Descartes’ Rule of Signs 1
Manuel Eberl
Added 13 Apr 2016
Updated 13 Apr 2016
Type Journal
Year 2015
Where AFP
Authors Manuel Eberl
Comments (0)