src/HOL/Limits.thy

 
 lemma tendsto_mult_right: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. (f x) * c) \<longlongrightarrow> l * c) F"
   for c :: "'a::topological_semigroup_mult"
   by (rule tendsto_mult [OF _ tendsto_const])
 
+lemma real_tendsto_mult_left_iff:
+   "c \<noteq> 0 \<Longrightarrow> tendsto(\<lambda>x. c * f x) (c * l) F \<longleftrightarrow> tendsto f l F" for c :: real
+  by (auto simp: tendsto_mult_left dest: tendsto_mult_left [where c = "1/c"])
+
+lemma real_tendsto_mult_right_iff:
+   "c \<noteq> 0 \<Longrightarrow> tendsto(\<lambda>x. f x * c) (l * c) F \<longleftrightarrow> tendsto f l F" for c :: real
+  by (simp add: mult.commute real_tendsto_mult_left_iff)
+
 lemma lim_const_over_n [tendsto_intros]:
   fixes a :: "'a::real_normed_field"
   shows "(\<lambda>n. a / of_nat n) \<longlonglongrightarrow> 0"
   using tendsto_mult [OF tendsto_const [of a] lim_1_over_n] by simp