# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1570628350 -3600
# Node ID 2d658afa1fc0182b0901681e7f3dcdc96468c6ab
# Parent  160eaf566bcb5581995b4c25d19ecf2b61ef12ff
Generalised two results concerning limits from the real numbers to type classes

diff -r 160eaf566bcb -r 2d658afa1fc0 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue Oct 08 10:26:40 2019 +0000
+++ b/src/HOL/Limits.thy	Wed Oct 09 14:39:10 2019 +0100
@@ -779,13 +779,13 @@
   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
+lemma tendsto_mult_left_iff:
+   "c \<noteq> 0 \<Longrightarrow> tendsto(\<lambda>x. c * f x) (c * l) F \<longleftrightarrow> tendsto f l F" for c :: "'a::{topological_semigroup_mult,field}"
   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 tendsto_mult_right_iff:
+   "c \<noteq> 0 \<Longrightarrow> tendsto(\<lambda>x. f x * c) (l * c) F \<longleftrightarrow> tendsto f l F" for c :: "'a::{topological_semigroup_mult,field}"
+  by (auto simp: tendsto_mult_right dest: tendsto_mult_left [where c = "1/c"])
 
 lemma lim_const_over_n [tendsto_intros]:
   fixes a :: "'a::real_normed_field"