Theorems · Theorem · field theory

Polynomial.signVariations_eq_eraseLead_add_ite

∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] {P : Polynomial R},
  P ≠ 0 →
    P.signVariations =
      P.eraseLead.signVariations +
        if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0

If we drop the leading coefficient, the sign changes drop by 0 or 1 depending on whether the first two nonzero coefficients match.

Defined in

Mathlib.Algebra.Polynomial.RuleOfSigns

Cited by

1 results in Mathlib

Foundations

Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringLinearOrder