Theorems · Theorem · field theory

Polynomial.signVariations_X_sub_C_mul_eraseLead_le

∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {P : Polynomial R} {η : R},
  0 < P.leadingCoeff →
    0 < P.nextCoeff →
      ((Polynomial.X - Polynomial.C η) * P.eraseLead).signVariations ≤
        ((Polynomial.X - Polynomial.C η) * P).signVariations

If a polynomial starts with two positive coefficients, then the sign changes in the product (X - η) * P is the same as (X - η) * P.eraseLead. This lemma lets us do induction on the degree of P when P starts with matching coefficient signs. Of course this is also true when the first two coefficients of P are negative, but we just prove the case where they're positive since it's cleaner and sufficient for the later use.

Defined in

Mathlib.Algebra.Polynomial.RuleOfSigns

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingLinearOrderIsStrictOrderedRing