Theorem: tendsto_funscale (PrimeNumberTheoremAnd/Sobolev.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
f : ℝ → E
hf : ContinuousAt f 0
x : ℝ
⊢ Tendsto (fun R => R⁻¹ • x) atTop (𝓝 0)
Tactic:
simpa using tendsto_inv_atTop_zero.mul_const x
State after:
no goals