English
Let P be monic and split over algebraMap K L. Then for any r ∈ L, aeval r P.derivative equals P.leadingCoeff times the product over roots with r removed, mapped by (r - a).
Русский
Пусть P монически и распадается над алгебраMap K L. Тогда для любого r ∈ L aeval r P.derivative равно P.leadingCoeff умножить на произведение (r - a) по всем корням, кроме r.
LaTeX
$$$P.Monic \land P.Splits (algebraMap K L) \Rightarrow \forall r:\,L, aeval\ r\ P.derivative = P.leadingCoeff \cdot \prod_{a\in P.aroots L\setminus\{r\}} (r - a)$$$
Lean4
theorem aeval_derivative_of_splits [Algebra K L] [DecidableEq L] {P : K[X]} (hP : P.Splits (algebraMap K L)) (r : L) :
aeval r P.derivative =
algebraMap K L P.leadingCoeff * ((P.aroots L).map fun a ↦ (((P.aroots L).erase a).map (r - ·)).prod).sum :=
eval₂_derivative_of_splits hP r
