Theorems · Theorem · field theory

Polynomial.iterate_derivative_X_sub_pow

∀ {R : Type u} [inst : CommRing R] (n k : ℕ) (c : R),
  (⇑Polynomial.derivative)^[k] ((Polynomial.X - Polynomial.C c) ^ n) =
    n.descFactorial k • (Polynomial.X - Polynomial.C c) ^ (n - k)

Defined in

Mathlib.Algebra.Polynomial.Derivative

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommRing