### Abstract

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.

### License

BSD License

### Topics

- Mathematics/Analysis

### Session Descartes_Sign_Rule

- Descartes_Sign_Rule

### Used by

- Chebyshev Polynomials
- A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL

## Cite

×

Descartes_Sign_Rule-AFP

    @article{Descartes_Sign_Rule-AFP,
      author  = {Manuel Eberl},
      title   = {Descartes' Rule of Signs},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2015},
      note    = {\url{https://isa-afp.org/entries/Descartes_Sign_Rule.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- Jan 5, 2016 : Isabelle2015