Theorem: iteratedFDeriv_neg_apply' (ForML/Util.lean)

State before:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : Semiring 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : SMulCommClass 𝕜 𝕜' F
inst✝ : ContinuousConstSMul 𝕜' F
x : E
i : ℕ
f : E → F
⊢ iteratedFDeriv 𝕜 i (fun x => -f x) x = -iteratedFDeriv 𝕜 i f x
Tactic:
rw [← iteratedFDeriv_neg_apply]
State after:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : Semiring 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : SMulCommClass 𝕜 𝕜' F
inst✝ : ContinuousConstSMul 𝕜' F
x : E
i : ℕ
f : E → F
⊢ iteratedFDeriv 𝕜 i (fun x => -f x) x = iteratedFDeriv 𝕜 i (-f) x

State before:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : Semiring 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : SMulCommClass 𝕜 𝕜' F
inst✝ : ContinuousConstSMul 𝕜' F
x : E
i : ℕ
f : E → F
⊢ iteratedFDeriv 𝕜 i (fun x => -f x) x = iteratedFDeriv 𝕜 i (-f) x
Tactic:
rfl
State after:
no goals