--- a/src/HOL/Limits.thy Thu Jul 11 18:37:52 2019 +0200
+++ b/src/HOL/Limits.thy Wed Jul 17 14:02:42 2019 +0100
@@ -779,6 +779,11 @@
for c :: "'a::topological_semigroup_mult"
by (rule tendsto_mult [OF _ tendsto_const])
+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
+
lemmas continuous_of_real [continuous_intros] =
bounded_linear.continuous [OF bounded_linear_of_real]