simpa using (hasDerivAt_id v).const_smul R⁻¹
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f✝ : CS n E
R x v✝ : ℝ
f : CS (n + 1) E
v : ℝ
hR : ¬R = 0
⊢ HasDerivAt (HSMul.hSMul R⁻¹) R⁻¹ v
no goals