English
For any natural number k, the k-th iterate of the derivative is k! times the k-th Hasse derivative: (derivative(R))^[k] f = k! · hasseDeriv(R, k) f.
Русский
Для любого натурального k последовательность применения производной к f после k раз равно k! умножить на k-ую производную Хассе: (derivative(R))^[k] f = k! · hasseDeriv(R, k) f.
LaTeX
$$$(\mathrm{derivative}(R))^{[k]} f = k! \cdot \mathrm{hasseDeriv}(R,k)\, f$$
Lean4
theorem derivative_iterate (k : ℕ) (f : LaurentSeries V) : (derivative R)^[k] f = k.factorial • (hasseDeriv R k f) :=
by
ext n
induction k generalizing f with
| zero => simp
| succ k ih =>
rw [Function.iterate_succ, Function.comp_apply, ih, derivative_apply, hasseDeriv_comp, Nat.choose_symm_add,
Nat.choose_one_right, Nat.factorial, mul_nsmul]
