no goals
α : Type u_3
β : Type u_2
𝕜 : Type u_1
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : TopologicalSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMulWithZero 𝕜 β
inst✝ : ContinuousSMul 𝕜 β
l : Filter α
f : α → β
c : 𝕜
hf : ZeroAtFilter l f
⊢ ZeroAtFilter l (c • f)
simpa using hf.const_smul c