𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_1
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type ?u.103039
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
m : Fin n → 𝕜
⊢ ↑(iteratedFDeriv 𝕜 n f x) m = ↑(iteratedFDeriv 𝕜 n f x) fun i => m i • 1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_1
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type ?u.103039
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
m : Fin n → 𝕜
⊢ ↑(iteratedFDeriv 𝕜 n f x) m = (∏ i : Fin n, m i) • iteratedDeriv n f x
rw [iteratedDeriv_eq_iteratedFDeriv, ← ContinuousMultilinearMap.map_smul_univ]
no goals
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_1
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type ?u.103039
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
m : Fin n → 𝕜
⊢ ↑(iteratedFDeriv 𝕜 n f x) m = ↑(iteratedFDeriv 𝕜 n f x) fun i => m i • 1
simp