Theorems · Definition · field theory
Polynomial.signVariations
{R : Type u_1} → [inst : Semiring R] → [LinearOrder R] → Polynomial R → ℕCounts the number of times that the coefficients in a polynomial change sign, with the convention that 0 can count as either sign.
- Defined in
- Mathlib.Algebra.Polynomial.RuleOfSigns
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SemiringLinearOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Semiringstatement and proof · cited by 13,802
- LinearOrderstatement and proof · cited by 8,572
- Polynomialstatement and proof · cited by 5,681
- SignTypeproof · cited by 318
- SignType.signproof · cited by 128
- List.destutterproof · cited by 25
- Polynomial.coeffListproof · cited by 22
Cited by13
Results whose statement or proof uses this declaration.
- Polynomial.signVariations_zerostatement · cited by 4
- Polynomial.signVariations_negstatement and proof · cited by 2
- Polynomial.signVariations_eq_eraseLead_add_itestatement and proof · cited by 1
- Polynomial.signVariations_eraseLead_lestatement and proof · cited by 1
- Polynomial.succ_signVariations_le_X_sub_C_mulstatement and proof · cited by 1
- Polynomial.signVariations_X_sub_C_mul_eraseLead_lestatement · cited by 0
- Polynomial.signVariations_eraseLeadstatement and proof · cited by 0
- Polynomial.signVariations_eraseLead_mul_X_sub_Cstatement and proof · cited by 0
- Polynomial.signVariations_le_eraseLead_succstatement and proof · cited by 0
- Polynomial.signVariations_monomialstatement and proof · cited by 0
- Polynomial.succ_signVariations_X_sub_C_mul_monomialstatement · cited by 0
- Polynomial.roots_countP_pos_le_signVariationsstatement and proof · cited by 0