Theorems · Theorem · complex analysis

Polynomial.sum_derivRootWeight_pos

∀ {P : Polynomial ℂ}, 0 < P.degree → ∀ (z : ℂ), 0 < ∑ w ∈ P.roots.toFinset, P.derivRootWeight z w

The sum of the weights derivRootWeight P z w of all the roots w of P is positive, provided that P is not a constant polynomial.

Defined in

Mathlib.Analysis.Complex.Polynomial.GaussLucas

Cited by

2 results in Mathlib

Foundations

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