eval_derivative_of_splits — Mathlib

English

If a polynomial f splits under RingHom.id K, then it splits under any i: K →+* L.

Русский

Если f распадается под RingHom.id K, то распадается и через любой i: K →+* L.

LaTeX

$$$Splits\ (RingHom.id\ K)\ f \Rightarrow Splits\ i\ f$$$

Lean4

theorem eval_derivative_of_splits [DecidableEq K] {P : K[X]} (hP : P.Splits (.id K)) (r : K) :
    eval r P.derivative = P.leadingCoeff * (P.roots.map fun a ↦ ((P.roots.erase a).map (r - ·)).prod).sum := by
  simpa using eval₂_derivative_of_splits hP r

Похожие утверждения