Order

📁 Source: Mathlib/Analysis/Polynomial/Order.lean

Statistics

Metric	Count
Definitions	0
Theorems eval_le_zero_of_roots_le_of_leadingCoeff_nonpos, eval_lt_zero_of_roots_lt_of_leadingCoeff_nonpos, negOnePow_mul_eval_le_zero_of_le_roots_of_leadingCoeff_nonpos, negOnePow_mul_eval_lt_zero_of_lt_roots_of_leadingCoeff_nonpos, zero_le_eval_of_roots_le_of_leadingCoeff_nonneg, zero_le_negOnePow_mul_eval_of_le_roots_of_leadingCoeff_nonneg, zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg, zero_lt_negOnePow_mul_eval_of_lt_roots_of_leadingCoeff_nonneg	8
Total	8

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eval_le_zero_of_roots_le_of_leadingCoeff_nonpos 📖	mathematical	Real Real.instLE leadingCoeff Real.semiring Real.instZero	Real Real.instLE eval Real.semiring Real.instZero	—	zero_le_eval_of_roots_le_of_leadingCoeff_nonneg IsRoot.eq_1 neg_zero neg_eq_iff_eq_neg eval_neg leadingCoeff_neg neg_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
eval_lt_zero_of_roots_lt_of_leadingCoeff_nonpos 📖	mathematical	Real Real.instLT Real.instLE leadingCoeff Real.semiring Real.instZero	Real Real.instLT eval Real.semiring Real.instZero	—	zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg IsRoot.eq_1 neg_zero neg_eq_iff_eq_neg eval_neg leadingCoeff_neg le_neg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid
negOnePow_mul_eval_le_zero_of_le_roots_of_leadingCoeff_nonpos 📖	mathematical	Real Real.instLE leadingCoeff Real.semiring Real.instZero	Real Real.instLE Real.instMul Real.instIntCast Units.val Int.instMonoid Int.negOnePow natDegree Real.semiring eval Real.instZero	—	zero_le_negOnePow_mul_eval_of_le_roots_of_leadingCoeff_nonneg IsRoot.eq_1 neg_zero neg_eq_iff_eq_neg eval_neg leadingCoeff_neg neg_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Int.coe_negOnePow natDegree_neg mul_neg
negOnePow_mul_eval_lt_zero_of_lt_roots_of_leadingCoeff_nonpos 📖	mathematical	Real Real.instLT Real.instLE leadingCoeff Real.semiring Real.instZero	Real Real.instLT Real.instMul Real.instIntCast Units.val Int.instMonoid Int.negOnePow natDegree Real.semiring eval Real.instZero	—	zero_lt_negOnePow_mul_eval_of_lt_roots_of_leadingCoeff_nonneg IsRoot.eq_1 neg_zero neg_eq_iff_eq_neg eval_neg leadingCoeff_neg le_neg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid Int.coe_negOnePow natDegree_neg mul_neg
zero_le_eval_of_roots_le_of_leadingCoeff_nonneg 📖	mathematical	Real Real.instLE Real.instZero leadingCoeff Real.semiring	Real Real.instLE Real.instZero eval Real.semiring	—	eq_of_le_of_ge le_refl LT.lt.le zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg Mathlib.Tactic.Push.not_and_eq
zero_le_negOnePow_mul_eval_of_le_roots_of_leadingCoeff_nonneg 📖	mathematical	Real Real.instLE Real.instZero leadingCoeff Real.semiring	Real Real.instLE Real.instZero Real.instMul Real.instIntCast Units.val Int.instMonoid Int.negOnePow natDegree Real.semiring eval	—	eq_of_ge_of_le MulZeroClass.mul_zero le_refl LT.lt.le zero_lt_negOnePow_mul_eval_of_lt_roots_of_leadingCoeff_nonneg Mathlib.Tactic.Push.not_and_eq
zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg 📖	mathematical	Real Real.instLT Real.instLE Real.instZero leadingCoeff Real.semiring	Real Real.instLT Real.instZero eval Real.semiring	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq leadingCoeff_eq_zero eq_of_le_of_ge eval_zero le_refl eq_C_of_degree_le_zero natDegree_eq_zero_iff_degree_le_zero eval_C Filter.Eventually.exists_forall_of_atTop instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean Filter.Tendsto.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instNontrivial tendsto_atTop_of_leadingCoeff_nonneg Real.instIsStrictOrderedRing instOrderTopologyReal LT.lt.le le_max_left le_max_right Set.mem_image intermediate_value_Icc LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Continuous.continuousOn continuous IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal
zero_lt_negOnePow_mul_eval_of_lt_roots_of_leadingCoeff_nonneg 📖	mathematical	Real Real.instLT Real.instLE Real.instZero leadingCoeff Real.semiring	Real Real.instLT Real.instZero Real.instMul Real.instIntCast Units.val Int.instMonoid Int.negOnePow natDegree Real.semiring eval	—	comp_neg_X_leadingCoeff_eq Int.coe_negOnePow Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right natDegree_comp NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass natDegree_neg natDegree_X Real.instNontrivial mul_one mul_comm mul_assoc IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing AddGroup.existsAddOfLE IsStrictOrderedRing.toPosMulStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_lt_of_covariant_le isReduced_of_noZeroDivisors NeZero.charZero_one RCLike.charZero_rclike Nat.even_or_odd Int.negOnePow_even Int.cast_one one_mul zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg eval_comp eval_neg eval_X neg_neg Int.negOnePow_odd Int.cast_neg neg_one_mul eval_lt_zero_of_roots_lt_of_leadingCoeff_nonpos nonpos_of_neg_nonneg neg_pos

---

← Back to Index