Theorems · Theorem · complex analysis

Polynomial.eq_centerMass_of_eval_derivative_eq_zero

• 1000+ list: Gauss–Lucas theorem

∀ {P : Polynomial ℂ} {z : ℂ},
  0 < P.degree →
    Polynomial.eval z (Polynomial.derivative P) = 0 → z = P.roots.toFinset.centerMass (P.derivRootWeight z) id

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$. This version provides explicit formulas for the coefficients of the convex combination. See also rootSet_derivative_subset_convexHull_rootSet below.

Defined in

Mathlib.Analysis.Complex.Polynomial.GaussLucas

Cited by

1 results in Mathlib

Foundations

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