no goals
α : Type u_2
β : Type u_1
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : CommSemiring β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
c : β
z : ℕ
⊢ Tendsto (fun a => k a ^ z * (fun n => f n * c) a) l (𝓝 0)
simpa only [← mul_assoc, MulZeroClass.zero_mul] using Tendsto.mul_const c (hf z)