Polynomial

📁 Source: Mathlib/Analysis/Calculus/LocalExtr/Polynomial.lean

Statistics

Metric	Count
Definitions	0
Theorems card_rootSet_le_derivative, card_roots_le_derivative, card_roots_toFinset_le_card_roots_derivative_diff_roots_succ, card_roots_toFinset_le_derivative	4
Total	4

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_rootSet_le_derivative 📖	mathematical	—	Fintype.card Set.Elem Real rootSet Real.commRing Real.instIsDomain rootSetFintype DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	Real.instIsDomain Fintype.card_congr' rootSet_def Fintype.card_coe roots.congr_simp derivative_map card_roots_toFinset_le_derivative
card_roots_le_derivative 📖	mathematical	—	Multiset.card Real roots Real.commRing Real.instIsDomain DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	Real.instIsDomain Multiset.toFinset_sum_count_eq Finset.sum_congr tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub Multiset.count_pos Multiset.mem_toFinset count_roots Finset.sum_add_distrib Finset.card_eq_sum_ones add_le_add covariant_swap_add_of_covariant_add Finset.sum_le_sum rootMultiplicity_sub_one_le_derivative_rootMultiplicity NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing card_roots_toFinset_le_card_roots_derivative_diff_roots_succ add_le_add_right add_le_add_left Finset.mem_sdiff add_assoc Finset.sum_union Finset.disjoint_sdiff Finset.union_sdiff_self_eq_union Finset.sum_subset Finset.subset_union_right
card_roots_toFinset_le_card_roots_derivative_diff_roots_succ 📖	mathematical	—	Finset.card Real Multiset.toFinset Real.decidableEq roots Real.commRing Real.instIsDomain Finset Finset.instSDiff DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	Real.instIsDomain eq_or_ne eq_C_of_derivative_eq_zero instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add roots_C Multiset.toFinset_zero Finset.card_empty zero_le Nat.instCanonicallyOrderedAdd derivative_zero Finset.card_le_diff_of_interleaved exists_deriv_eq_zero continuousOn IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal mem_roots Multiset.mem_toFinset IsRoot.eq_1 deriv
card_roots_toFinset_le_derivative 📖	mathematical	—	Finset.card Real Multiset.toFinset Real.decidableEq roots Real.commRing Real.instIsDomain DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	LE.le.trans Real.instIsDomain card_roots_toFinset_le_card_roots_derivative_diff_roots_succ le_imp_le_of_le_of_le add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Finset.card_le_card Finset.sdiff_subset le_refl

---

← Back to Index