Power series coefficient facts #
theorem
iteratedDeriv_id_smul
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{f : 𝕜 → E}
{n : ℕ}
(fc : ContDiff 𝕜 (↑n) f)
{y : 𝕜}
:
iteratedDeriv n (fun (x : 𝕜) => x • f x) y = y • iteratedDeriv n f y + n • iteratedDeriv (n - 1) f y