Theorems · Theorem · field theory

Polynomial.aeval_sumIDeriv_eq_eval

∀ {R : Type u_1} [inst : CommSemiring R] (A : Type u_3) [inst_1 : CommRing A] [inst_2 : Algebra R A] (p : Polynomial R)
  (r : A),
  (Polynomial.aeval r) (Polynomial.sumIDeriv p) =
    Polynomial.eval r (Polynomial.sumIDeriv (Polynomial.map (algebraMap R A) p))

Defined in

Mathlib.Algebra.Polynomial.SumIteratedDerivative

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommRingAlgebra