--- a/src/HOL/Limits.thy Wed Sep 11 20:48:10 2019 +0200
+++ b/src/HOL/Limits.thy Thu Sep 12 14:51:45 2019 +0100
@@ -779,6 +779,14 @@
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"