English
If p splits over id and x ∈ L, then eval₂ f x p.derivative equals the leadingCoeff of p times the sum of products formed by removing each root in turn and evaluating at x.
Русский
Если p распадается над идентичным отображением и x ∈ L, то eval₂ f x p.derivative равно ведущему коэффициенту p, умноженному на сумму произведений, полученных при удалении каждого корня поочередно и подстановке x.
LaTeX
$$$\forall p:K[X],\forall x:L,\text{Splits (RingHom.id K) } p \Rightarrow eval_2\ f\ x\ p.derivative = p.leadingCoeff \cdot \sum_{a\in p.roots} \prod_{b\in p.roots\setminus\{a\}} (x-b)$$$
Lean4
theorem eval₂_derivative_of_splits [DecidableEq L] {P : K[X]} {f : K →+* L} (hP : P.Splits f) (x : L) :
eval₂ f x P.derivative =
f (P.leadingCoeff) * ((P.map f).roots.map fun a ↦ (((P.map f).roots.erase a).map (x - ·)).prod).sum :=
by
conv_lhs => rw [← eval_map, ← derivative_map, eq_prod_roots_of_splits hP]
classical simp [derivative_prod, eval_multisetSum, eval_multiset_prod]
