Theorem: iteratedDeriv_const_smul' (ForML/Util.lean)

State before:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜'
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
i : ℕ
c : 𝕜'
f : 𝕜 → F
x : 𝕜
hf : ContDiff 𝕜 (↑i) f
⊢ iteratedDeriv i (fun x => c • f x) x = c • iteratedDeriv i f x
Tactic:
simp only [iteratedDeriv_eq_iteratedFDeriv, ← Pi.smul_def]
State after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜'
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
i : ℕ
c : 𝕜'
f : 𝕜 → F
x : 𝕜
hf : ContDiff 𝕜 (↑i) f
⊢ ((iteratedFDeriv 𝕜 i (c • fun i => f i) x) fun x => 1) = c • (iteratedFDeriv 𝕜 i f x) fun x => 1

State before:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜'
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
i : ℕ
c : 𝕜'
f : 𝕜 → F
x : 𝕜
hf : ContDiff 𝕜 (↑i) f
⊢ ((iteratedFDeriv 𝕜 i (c • fun i => f i) x) fun x => 1) = c • (iteratedFDeriv 𝕜 i f x) fun x => 1
Tactic:
rw [iteratedFDeriv_const_smul_apply hf]
State after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜'
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
i : ℕ
c : 𝕜'
f : 𝕜 → F
x : 𝕜
hf : ContDiff 𝕜 (↑i) f
⊢ ((c • iteratedFDeriv 𝕜 i f x) fun x => 1) = c • (iteratedFDeriv 𝕜 i f x) fun x => 1

State before:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜'
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
i : ℕ
c : 𝕜'
f : 𝕜 → F
x : 𝕜
hf : ContDiff 𝕜 (↑i) f
⊢ ((c • iteratedFDeriv 𝕜 i f x) fun x => 1) = c • (iteratedFDeriv 𝕜 i f x) fun x => 1
Tactic:
simp
State after:
no goals