no goals
α : Type u_1
β : Type u_2
l✝ : Filter α
k✝ f g g' : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
l : Filter α
k : α → β
z : ℕ
⊢ Tendsto (fun a => k a ^ z * OfNat.ofNat 0 a) l (𝓝 0)
simpa only [Pi.zero_apply, MulZeroClass.mul_zero] using tendsto_const_nhds