hasseDeriv_comp_coeff — Mathlib

English

Composition of Hasse derivatives satisfies a binomial-type composition formula: D_k(D_l(f)) = C(k+l,k) D_{k+l}(f).

Русский

Сложение дифференцирования Хассе даёт формулу типа биномиала: D_k(D_l(f)) = binom(k+l,k) D_{k+l}(f).

LaTeX

$$hasseDeriv R k (hasseDeriv R l f) = (k+l).choose k • hasseDeriv R (k+l) f$$

Lean4

theorem hasseDeriv_comp_coeff (k l : ℕ) (f : LaurentSeries V) (n : ℤ) :
    (hasseDeriv R k (hasseDeriv R l f)).coeff n = ((Nat.choose (k + l) k) • hasseDeriv R (k + l) f).coeff n :=
  by
  rw [coeff_nsmul]
  simp only [hasseDeriv_coeff, Pi.smul_apply, Nat.cast_add]
  rw [smul_smul, mul_comm, ← Ring.choose_add_smul_choose (n + k), add_assoc, Nat.choose_symm_add, smul_assoc]

Похожие утверждения