src/HOL/Real_Vector_Spaces.thy

--- a/src/HOL/Real_Vector_Spaces.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -148,6 +148,10 @@
     by simp
 qed
 
+lemma linear_scale_real:
+  fixes r::real shows "linear f \<Longrightarrow> f (r * b) = r * f b"
+  using linear_scale by fastforce
+
 interpretation scaleR_left: additive "(\<lambda>a. scaleR a x :: 'a::real_vector)"
   by standard (rule scaleR_left_distrib)