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
⊢ SuperpolynomialDecay l k (f * k) ↔ SuperpolynomialDecay l k f
simpa [mul_comm k] using superpolynomialDecay_param_mul_iff f hk