Theorems · Theorem · field theory

Polynomial.Splits.eval_derivative

∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [inst_1 : IsDomain R] [inst_2 : DecidableEq R],
  f.Splits →
    ∀ (x : R),
      Polynomial.eval x (Polynomial.derivative f) =
        f.leadingCoeff *
          (Multiset.map (fun a => (Multiset.map (fun x_1 => x - x_1) (f.roots.erase a)).prod) f.roots).sum

Defined in

Mathlib.Algebra.Polynomial.Splits

Cited by

1 results in Mathlib

Foundations

Depth 138 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomainDecidableEq