Documentation Verification Report

RuleOfSigns

📁 Source: Mathlib/Algebra/Polynomial/RuleOfSigns.lean

Statistics

Metric	Count
Definitions `signVariations`	1
Theorems `roots_countP_pos_le_signVariations`, `signVariations_C_mul`, `signVariations_X_sub_C_mul_eraseLead_le`, `signVariations_eq_eraseLead_add_ite`, `signVariations_eraseLead`, `signVariations_eraseLead_le`, `signVariations_eraseLead_mul_X_sub_C`, `signVariations_le_eraseLead_succ`, `signVariations_monomial`, `signVariations_neg`, `signVariations_zero`, `succ_signVariations_X_sub_C_mul_monomial`, `succ_signVariations_le_X_sub_C_mul`	13
Total	14

Polynomial

Definitions

Name	Category	Theorems
`signVariations` 📖	CompOp	13 math math: `signVariations_le_eraseLead_succ`, `signVariations_zero`, `signVariations_eraseLead`, `signVariations_eraseLead_le`, `signVariations_eraseLead_mul_X_sub_C`, `signVariations_monomial`, `signVariations_X_sub_C_mul_eraseLead_le`, `signVariations_neg`, `succ_signVariations_X_sub_C_mul_monomial`, `signVariations_eq_eraseLead_add_ite`, `roots_countP_pos_le_signVariations`, `succ_signVariations_le_X_sub_C_mul`, `signVariations_C_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`roots_countP_pos_le_signVariations` 📖	mathematical	—	`Multiset.countP` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearOrder.toDecidableLT` `roots` `IsStrictOrderedRing.isDomain` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddGroup.existsAddOfLE` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Preorder.toLE` `signVariations`	—	`IsStrictOrderedRing.isDomain` `AddGroup.existsAddOfLE` `zero_le` `Nat.instCanonicallyOrderedAdd` `dvd_iff_isRoot` `isRoot_of_mem_roots` `le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Multiset.countP_congr` `roots_mul` `ne_zero_of_mem_roots` `roots_X_sub_C` `Multiset.countP_cons_of_pos` `le_refl` `succ_signVariations_le_X_sub_C_mul` `right_ne_zero_of_mul`
`signVariations_C_mul` 📖	mathematical	—	`signVariations` `Ring.toSemiring` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`signVariations.eq_1` `coeffList_C_mul` `IsStrictOrderedRing.noZeroDivisors` `AddGroup.existsAddOfLE` `lt_or_lt_iff_ne` `List.comp_map` `sign_mul` `sign_pos` `one_mul` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `lt_of_le_of_ne` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `mul_neg` `neg_mul` `neg_neg` `signVariations_neg`
`signVariations_X_sub_C_mul_eraseLead_le` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `leadingCoeff` `Ring.toSemiring` `nextCoeff`	`signVariations` `Polynomial` `instMul` `instSub` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `eraseLead`	—	`LT.lt.ne'` `sign_pos` `Nat.instOrderedSub` `List.length_pos_of_ne_nil` `List.destutter'_ne_nil` `List.destutter'.congr_simp` `le_refl` `List.destutter'_cons` `zero_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instZeroLEOneClass` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `List.destutter_cons'`
`signVariations_eq_eraseLead_add_ite` 📖	mathematical	—	`signVariations` `eraseLead` `SignType` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `LinearOrder.toDecidableLT` `leadingCoeff` `SignType.instNeg` `instDecidableEqSignType`	—	`signVariations.eq_1` `coeffList_eraseLead` `List.destutter.congr_simp` `coeffList_eq_nil` `tsub_zero` `Nat.instOrderedSub` `sign_zero` `zero_add` `tsub_self` `Nat.instCanonicallyOrderedAdd` `zero_tsub` `neg_zero` `add_zero` `coeffList_eq_cons_leadingCoeff`
`signVariations_eraseLead` 📖	mathematical	`DFunLike.coe` `OrderHom` `SignType` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `LinearOrder.toDecidableLT` `leadingCoeff` `nextCoeff`	`signVariations` `eraseLead`	—	`eraseLead_zero` `signVariations_zero` `sign_zero` `coeffList_eq_cons_leadingCoeff` `nextCoeff_eq_zero_of_eraseLead_eq_zero` `leadingCoeff_eraseLead_eq_nextCoeff` `coeffList_eraseLead` `List.destutter'_cons_neg`
`signVariations_eraseLead_le` 📖	mathematical	—	`signVariations` `eraseLead`	—	`eraseLead_zero` `signVariations_zero`
`signVariations_eraseLead_mul_X_sub_C` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `leadingCoeff` `Ring.toSemiring` `nextCoeff`	`signVariations` `eraseLead` `Polynomial` `instMul` `instSub` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`natDegree_pos_of_nextCoeff_ne_zero` `LT.lt.ne` `leadingCoeff_ne_zero` `LT.lt.ne'` `natDegree_mul` `IsStrictOrderedRing.noZeroDivisors` `AddGroup.existsAddOfLE` `X_sub_C_ne_zero` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `natDegree_X_sub_C` `add_comm` `nextCoeff_eq_zero_of_eraseLead_eq_zero` `natDegree_eraseLead_add_one` `sub_neg` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `self_sub_monomial_natDegree_leadingCoeff` `leadingCoeff_eraseLead_eq_nextCoeff` `leadingCoeff_monic_mul` `monic_X_sub_C` `mul_sub` `sub_mul` `X_mul_monomial` `C_mul_monomial` `monomial_sub` `leadingCoeff.eq_1` `nextCoeff_of_natDegree_pos` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `signVariations.eq_1`
`signVariations_le_eraseLead_succ` 📖	mathematical	—	`signVariations` `eraseLead`	—	`signVariations_zero` `eraseLead_zero` `zero_add` `Nat.instCanonicallyOrderedAdd`
`signVariations_monomial` 📖	mathematical	—	`signVariations` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial`	—	`monomial_zero_right` `signVariations_zero` `List.destutter.congr_simp` `coeffList_eraseLead` `monomial_eq_zero_iff` `leadingCoeff_monomial` `natDegree_monomial` `eraseLead_monomial` `tsub_zero` `Nat.instOrderedSub` `coeffList_zero` `sign_zero` `zero_add` `tsub_self` `Nat.instCanonicallyOrderedAdd`
`signVariations_neg` 📖	mathematical	—	`signVariations` `Ring.toSemiring` `Polynomial` `instNeg`	—	`signVariations.eq_1` `coeffList_neg` `List.destutter.congr_simp` `List.comp_map`
`signVariations_zero` 📖	mathematical	—	`signVariations` `Polynomial` `instZero`	—	`List.destutter.congr_simp` `coeffList_zero` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub`
`succ_signVariations_X_sub_C_mul_monomial` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`signVariations` `Ring.toSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `instMul` `instSub` `X` `RingHom` `RingHom.instFunLike` `C`	—	`natDegree_mul` `IsStrictOrderedRing.noZeroDivisors` `AddGroup.existsAddOfLE` `X_sub_C_ne_zero` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `natDegree_sub_C` `natDegree_X` `natDegree_monomial` `add_tsub_cancel_left` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `zero_add` `coeff_sub` `coeff_X_zero` `coeff_C_zero` `zero_sub` `neg_mul` `coeff_mul_monomial` `nextCoeff_eq_zero_of_eraseLead_eq_zero` `LT.lt.ne'` `Left.sign_neg` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `sign_mul` `sign_pos` `one_mul` `List.destutter.congr_simp` `coeffList_eraseLead` `leadingCoeff_monomial` `eraseLead_monomial` `tsub_zero` `coeffList_zero` `sign_zero` `tsub_self` `Nat.instCanonicallyOrderedAdd` `leadingCoeff_mul` `leadingCoeff_X_sub_C` `leadingCoeff_eraseLead_eq_nextCoeff` `add_tsub_cancel_right` `List.length_pos_of_ne_nil` `List.destutter'_ne_nil`
`succ_signVariations_le_X_sub_C_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`signVariations` `Ring.toSemiring` `Polynomial` `instMul` `instSub` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`Nat.strong_induction_on` `mul_ne_zero` `instNoZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `AddGroup.existsAddOfLE` `X_sub_C_ne_zero` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `natDegree_mul` `natDegree_X_sub_C` `add_comm` `coeff_X_sub_C_mul` `zero_add` `coeff_eq_zero_of_natDegree_lt` `Nat.instZeroLEOneClass` `MulZeroClass.mul_zero` `sub_zero` `withBotSucc_degree_eq_natDegree_add_one` `List.destutter.congr_simp` `sign_pos` `NeZero.one` `GroupWithZero.toNontrivial` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `mul_coeff_zero` `coeff_sub` `coeff_X_zero` `coeff_C_zero` `zero_sub` `neg_mul` `sign_neg` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toPosMulStrictMono` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `List.destutter_pair` `leadingCoeff_mul` `leadingCoeff_X_sub_C` `one_mul` `SignType.trichotomy` `signVariations_eq_eraseLead_add_ite` `leadingCoeff_eraseLead_eq_nextCoeff` `neg_neg` `nextCoeff_eq_zero_of_eraseLead_eq_zero` `signVariations_eraseLead_le` `eraseLead_mul_eq_mul_eraseLead_of_nextCoeff_zero` `LT.lt.ne'` `add_tsub_cancel_right` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `contravariant_lt_of_covariant_le` `Nat.instIsOrderedAddMonoid` `add_zero` `Nat.instNoMaxOrder` `signVariations_neg` `mul_neg` `natDegree_neg`

---

← Back to Index