English
Let R be a semiring and f a Laurent series over R. Then the k-th Hasse derivative of the l-th Hasse derivative of f equals binomial(k+l, k) times the (k+l)-th Hasse derivative of f: hasseDeriv R k (hasseDeriv R l f) = (k + l).choose k • hasseDeriv R (k + l) f.
Русский
Пусть R — полугруппа (полугруппа с умножением и сложной алгеброй), f — лаурентовая (Laurent) серия над R. Тогда k-й производной Хассе от l-й производной Хассе от f равна биномиальному коэффициенту binom(k+l, k) умноженной на (k+l)-ю производную Хассе от f: hasseDeriv R k (hasseDeriv R l f) = (k+l choose k) • hasseDeriv R (k+l) f.
LaTeX
$$$\operatorname{hasseDeriv}_R(k)\big(\operatorname{hasseDeriv}_R(l) f\big) = \binom{k+l}{k}\,\operatorname{hasseDeriv}_R(k+l) f.$$$
Lean4
@[simp]
theorem hasseDeriv_comp (k l : ℕ) (f : LaurentSeries V) :
hasseDeriv R k (hasseDeriv R l f) = (k + l).choose k • hasseDeriv R (k + l) f :=
by
ext n
simp [hasseDeriv_comp_coeff k l f n]
