Descartes' Rule of Signs (Q7361156)
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 Descartes_Sign_Rule
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Descartes' Rule of Signs |
AFP entry Descartes_Sign_Rule |
Statements
28 December 2015
0 references
Manuel Eberl
0 references
Descartes' Rule of Signs (English)
0 references
Descartes' Rule of Signs relates the number of positive real roots of a polynomial with the number of sign changes in its coefficient sequence. Our proof follows the simple inductive proof given by Rob Arthan, 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.
0 references
