feat(topology/algebra/mul_action.lean): add smul_const (#7242)

add filter.tendsto.smul_const

Author: YaelDillies

src/topology/algebra/mul_action.lean

@@ -58,6 +58,11 @@ lemma filter.tendsto.const_smul {f : β → α} {l : filter β} {a : α} (hf : t
   tendsto (λ x, c • f x) l (𝓝 (c • a)) :=
 tendsto_const_nhds.smul hf
 
+lemma filter.tendsto.smul_const {f : β → M} {l : filter β} {c : M}
+  (hf : tendsto f l (𝓝 c)) (a : α) :
+  tendsto (λ x, (f x) • a) l (𝓝 (c • a)) :=
+hf.smul tendsto_const_nhds
+
 variables [topological_space β] {f : β → M} {g : β → α} {b : β} {s : set β}
 
 lemma continuous_within_at.smul (hf : continuous_within_at f s b)