English
If deg P > 0, the sum of weights over all roots of P is strictly positive.
Русский
Если deg P > 0, то сумма весов по всем корням P строго положительна.
LaTeX
$$0 < \\sum_{w \\in P.roots} \\operatorname{derivRootWeight}(z,w)$$
Lean4
/-- 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. -/
theorem sum_derivRootWeight_pos (hP : 0 < degree P) (z : ℂ) : 0 < ∑ w ∈ P.roots.toFinset, derivRootWeight P z w :=
by
have hP₀ : P ≠ 0 := by rintro rfl; simp at hP
by_cases hPz : P.eval z = 0
· simp [derivRootWeight, hPz, hP₀]
· simp only [derivRootWeight, if_neg hPz]
apply Finset.sum_pos
· intro w hw
apply div_pos (by simp_all)
suffices z ≠ w by simpa [sq_pos_iff, sub_eq_zero]
rintro rfl
simp_all
· rw [Multiset.toFinset_nonempty, ← P.map_id]
apply P.roots_ne_zero_of_splits _ (IsAlgClosed.splits _)
rwa [← pos_iff_ne_zero, natDegree_pos_iff_degree_pos]
