by_cases hR : R = 0 <;> simp [hR, scale, funscale]
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.scale R).toFun v = R⁻¹ • f.deriv.toFun (R⁻¹ • v)
no goals