Theorems · Theorem · complex analysis

Polynomial.rootSet_derivative_subset_convexHull_rootSet

• 1000+ list: Gauss–Lucas theorem

∀ {P : Polynomial ℂ}, 0 < P.degree → (Polynomial.derivative P).rootSet ℂ ⊆ (convexHull ℝ) (P.rootSet ℂ)

Gauss-Lucas Theorem: if $P$ is a nonconstant polynomial with complex coefficients, then all zeros of $P'$ belong to the convex hull of the set of zeros of $P$. See also eq_centerMass_of_eval_derivative_eq_zero for a version that provides explicit coefficients of the convex combination.

Defined in

Mathlib.Analysis.Complex.Polynomial.GaussLucas

Cited by

0 results in Mathlib

Foundations

Depth 298 from the axioms · uses propext, Classical.choice, Quot.sound