English
As in the earlier statement, if there exists a multiset s with f.map i equal to C (i f.leadingCoeff) times the product over (X - C a) for a in s, then f splits over i.
Русский
Как и ранее, если существует мультисет s такой, что f.map i = C (i leadingCoeff) · ∏_{a∈s}(X - C a), то f распадается через i.
LaTeX
$$$Splits\ i\ f \iff \exists s:Multiset\ L,\ f.map\ i = C(i\ f.leadingCoeff) \cdot (s.map (\lambda a. X - C a)).prod$$$
Lean4
/-- Let `P` be a monic polynomial over `K` that splits over `L`. Let `r : L` be a root of `P`.
Then $P'(r) = \prod_{a}(r-a)$, where the product in the RHS is taken over all roots of `P` in `L`,
with the multiplicity of `r` reduced by one. -/
theorem aeval_root_derivative_of_splits [Algebra K L] [DecidableEq L] {P : K[X]} (hmo : P.Monic)
(hP : P.Splits (algebraMap K L)) {r : L} (hr : r ∈ P.aroots L) :
aeval r (Polynomial.derivative P) = (((P.aroots L).erase r).map fun a => r - a).prod :=
by
replace hmo := hmo.map (algebraMap K L)
replace hP := (splits_id_iff_splits (algebraMap K L)).2 hP
rw [aeval_def, ← eval_map, ← derivative_map]
nth_rw 1 [eq_prod_roots_of_monic_of_splits_id hmo hP]
rw [eval_multiset_prod_X_sub_C_derivative hr]
