Theorems · Theorem · field theory

Polynomial.derivative_prod

∀ {R : Type u} {ι : Type y} [inst : CommSemiring R] [inst_1 : DecidableEq ι] {s : Multiset ι} {f : ι → Polynomial R},
  Polynomial.derivative (Multiset.map f s).prod =
    (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * Polynomial.derivative (f i)) s).sum

Defined in

Mathlib.Algebra.Polynomial.Derivative

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommSemiringDecidableEq