no goals
𝕜 : Type u_1
α : Type ?u.31571
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℕ
hn : n ≠ 0
⊢ Tendsto (fun x => x ^ (-↑n)) atTop (𝓝 0)
simpa only [zpow_neg, zpow_ofNat] using (@tendsto_pow_atTop 𝕜 _ _ hn).inv_tendsto_atTop