Polynomial.card_rootSet_le_derivative
theorem Polynomial.card_rootSet_le_derivative :
∀ {F : Type u_1} [inst : CommRing F] [inst_1 : Algebra F ℝ] (p : Polynomial F),
Fintype.card ↑(p.rootSet ℝ) ≤ Fintype.card ↑((Polynomial.derivative p).rootSet ℝ) + 1
This theorem states that for any polynomial `p` over a commutative ring `F` with an algebra structure over the real numbers, the number of real roots of `p` is less than or equal to the number of real roots of its derivative plus one. It implies that a polynomial cannot have more real roots than its degree (since the derivative of a polynomial has one degree less than the original polynomial).
More concisely: For any polynomial `p` over a commutative ring `F` with an algebra structure over the real numbers, the number of real roots of `p` is bounded above by the number of real roots of its derivative plus one.
|
Polynomial.card_roots_toFinset_le_derivative
theorem Polynomial.card_roots_toFinset_le_derivative :
∀ (p : Polynomial ℝ), p.roots.toFinset.card ≤ (Polynomial.derivative p).roots.toFinset.card + 1
The given theorem states that for any real polynomial `p`, the count of its roots is less than or equal to the count of roots of its derivative plus one. In other words, the number of distinct roots of a real polynomial does not exceed the number of distinct roots of its derivative by more than one.
More concisely: The number of real roots of a polynomial is bounded above by the number of real roots of its derivative plus one.
|
Polynomial.card_roots_toFinset_le_card_roots_derivative_diff_roots_succ
theorem Polynomial.card_roots_toFinset_le_card_roots_derivative_diff_roots_succ :
∀ (p : Polynomial ℝ),
p.roots.toFinset.card ≤ ((Polynomial.derivative p).roots.toFinset \ p.roots.toFinset).card + 1
This theorem states that for any real polynomial `p`, the number of distinct roots of `p` is bounded above by the number of distinct roots of its derivative that are not roots of `p` plus one. In other words, a polynomial cannot have more roots than one plus the number of unique roots of its derivative that are not also roots of the original polynomial.
More concisely: The number of distinct roots of a real polynomial is bounded above by the number of distinct roots of its derivative that are not roots of the polynomial plus one.
|
Polynomial.card_roots_le_derivative
theorem Polynomial.card_roots_le_derivative :
∀ (p : Polynomial ℝ), Multiset.card p.roots ≤ Multiset.card (Polynomial.derivative p).roots + 1
This theorem states that for any real polynomial `p`, the number of roots (accounting for multiplicities) is less than or equal to the number of roots (accounting for multiplicities) of its derivative plus one. In other words, a real polynomial can have at most one more root than its derivative.
More concisely: The number of real roots (accounting for multiplicities) of a real polynomial is fewer than or equal to the number of real roots of its derivative plus one.
|