no goals
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (k⁻¹ * f)
simpa using hf.param_zpow_mul hk (-1)