Theorem: iteratedDeriv_mul_const_apply (ForML/Trigonometric.lean)

State before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
a : 𝕜'
f : 𝕜 → 𝕜'
hf : ContDiff 𝕜 (↑n) f
x : 𝕜
⊢ iteratedDeriv n (fun x => f x * a) x = iteratedDeriv n f x * a
Tactic:
simp_rw [mul_comm _ a]
State after:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
a : 𝕜'
f : 𝕜 → 𝕜'
hf : ContDiff 𝕜 (↑n) f
x : 𝕜
⊢ iteratedDeriv n (fun x => a * f x) x = a * iteratedDeriv n f x

State before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
a : 𝕜'
f : 𝕜 → 𝕜'
hf : ContDiff 𝕜 (↑n) f
x : 𝕜
⊢ iteratedDeriv n (fun x => a * f x) x = a * iteratedDeriv n f x
Tactic:
exact iteratedDeriv_const_mul_apply a hf
State after:
no goals