src/HOL/Analysis/Cartesian_Euclidean_Space.thy
changeset 67971 e9f66b35d636
parent 67968 a5ad4c015d1c
parent 67969 83c8cafdebe8
child 67979 53323937ee25
     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Mon Apr 09 16:20:23 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Mon Apr 09 17:21:10 2018 +0100
     1.3 @@ -297,7 +297,7 @@
     1.4  lemma norm_le_l1_cart: "norm x <= sum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
     1.5    by (simp add: norm_vec_def L2_set_le_sum)
     1.6  
     1.7 -lemma scalar_mult_eq_scaleR: "c *s x = c *\<^sub>R x"
     1.8 +lemma scalar_mult_eq_scaleR [simp]: "c *s x = c *\<^sub>R x"
     1.9    unfolding scaleR_vec_def vector_scalar_mult_def by simp
    1.10  
    1.11  lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y"