Theorems · Theorem · field theory

Polynomial.aeval_iterate_derivative_self

∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A] (p : Polynomial R)
  (q : ℕ) (r : A) {p' : Polynomial A},
  Polynomial.map (algebraMap R A) p = (Polynomial.X - Polynomial.C r) ^ q * p' →
    (Polynomial.aeval r) ((⇑Polynomial.derivative)^[q] p) = q.factorial • Polynomial.eval r p'

Defined in

Mathlib.Algebra.Polynomial.SumIteratedDerivative

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommRingAlgebra