ext x
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v : ℝ
f : CS (n + 1) E
⊢ (R • f).deriv = R • f.deriv
case toFun.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x✝ v : ℝ
f : CS (n + 1) E
x : ℝ
⊢ (R • f).deriv.toFun x = (R • f.deriv).toFun x