simp [nnabla, mul_sub]
case h
n✝ : ℕ
A a b c✝ d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
inst✝ : Ring E
u : α → E
c : E
n : α
⊢ nnabla (fun n => c * u n) n = (c • nnabla u) n
no goals