English
If f splits after composing i with j, then f splits after i provided the same root-range condition
Русский
Если f распадается после композиции i и j, тогда f распадается и через i при условии того же ограничения корней
LaTeX
$$$\forall i:j,\,f:K[X],\ Splits (j .\, i) f \land (\forall a\in (f.map (j . i)).roots, a\in j.range) \Rightarrow Splits i f$$$
Lean4
theorem eval_derivative_eq_eval_mul_sum_of_splits {p : K[X]} {x : K} (h : p.Splits (.id K)) (hx : p.eval x ≠ 0) :
p.derivative.eval x = p.eval x * (p.roots.map fun z ↦ 1 / (x - z)).sum := by
classical
suffices
p.roots.map (fun z ↦ p.leadingCoeff * ((p.roots.erase z).map (fun w ↦ x - w)).prod) =
p.roots.map fun i ↦ p.leadingCoeff * ((x - i)⁻¹ * (p.roots.map (fun z ↦ x - z)).prod)
by
nth_rw 2 [p.eq_prod_roots_of_splits_id h]
simp [eval_derivative_of_splits h, ← Multiset.sum_map_mul_left, this, eval_multiset_prod, mul_comm, mul_left_comm]
refine Multiset.map_congr rfl fun z hz ↦ ?_
rw [← Multiset.prod_map_erase hz, inv_mul_cancel_left₀]
aesop (add simp sub_eq_zero)
