Iterated Leibniz rule

TheoremLeibniz rule for iterated derivations#✓fully proved

Leibniz's rule for an iterated derivation. The natural weights are not cancelled, so the identity remains valid in positive characteristic.

theorem iterate_mul (D : Derivation R B B) (n : ℕ) (a b : B) :
    (D : B → B)^[n] (a * b) =
      ∑ p ∈ Finset.antidiagonal n,
        n.choose p.1 • ((D : B → B)^[p.1] a * (D : B → B)^[p.2] b)

Used by 1

Used byFactorial-normalized iterated Leibniz rule

TheoremFactorial-normalized iterated Leibniz rule#✓fully proved

The factorial-normalized iterated Leibniz rule for a rational derivation.

theorem iterate_mul_div (D : Derivation ℚ B B) (n : ℕ) (a b : B) :
    ((n.factorial : ℚ)⁻¹) • (D : B → B)^[n] (a * b) =
      ∑ p ∈ Finset.antidiagonal n,
        ((p.1.factorial : ℚ)⁻¹ * (p.2.factorial : ℚ)⁻¹) •
          ((D : B → B)^[p.1] a * (D : B → B)^[p.2] b)

Uses 1 · Used by 1

Proof usesLeibniz rule for iterated derivations

Used byThe exponential of coefficient derivations is multiplicative

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.