Theorems · Theorem · field theory

Polynomial.aeval_sumIDeriv

∀ {R : Type u_1} [inst : CommSemiring R] (A : Type u_3) [inst_1 : CommRing A] [inst_2 : Algebra R A] (p : Polynomial R)
  (q : ℕ),
  ∃ gp,
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        (Polynomial.X - Polynomial.C r) ^ q ∣ Polynomial.map (algebraMap R A) p →
          (Polynomial.aeval r) (Polynomial.sumIDeriv p) = q.factorial • (Polynomial.aeval r) gp

Defined in

Mathlib.Algebra.Polynomial.SumIteratedDerivative

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommRingAlgebra