Iterated derivations and the Leibniz rule

• Iterated Leibniz rule

TheoremIterated derivation of a power when \(D\varepsilon = r\varepsilon^2\)#✓fully proved

If D epsilon = r • epsilon², then the nth iterate of D on epsilon^m has coefficient r^n times the ascending factorial of m. The coefficient is not cancelled, so the formula remains valid in positive characteristic.

theorem iterate_pow_of_apply_eq_smul_sq (D : Derivation R A A) (r : R) (epsilon : A)
    (h : D epsilon = r • epsilon ^ 2) (n m : ℕ) :
    (D : A → A)^[n] (epsilon ^ m) =
      (r ^ n * (m.ascFactorial n : R)) • epsilon ^ (m + n)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.