src/HOL/Real_Vector_Spaces.thy
changeset 62049 b0f941e207cf
parent 61976 3a27957ac658
child 62087 44841d07ef1d
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sun Jan 03 21:45:34 2016 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Jan 04 17:45:36 2016 +0100
     1.3 @@ -191,7 +191,7 @@
     1.4    fixes x :: "'a::real_vector"
     1.5    shows "scaleR (-1) x = - x"
     1.6    using scaleR_minus_left [of 1 x] by simp
     1.7 -
     1.8 +  
     1.9  class real_algebra = real_vector + ring +
    1.10    assumes mult_scaleR_left [simp]: "scaleR a x * y = scaleR a (x * y)"
    1.11    and mult_scaleR_right [simp]: "x * scaleR a y = scaleR a (x * y)"
    1.12 @@ -686,6 +686,10 @@
    1.13  
    1.14  class real_normed_algebra_1 = real_algebra_1 + real_normed_algebra +
    1.15    assumes norm_one [simp]: "norm 1 = 1"
    1.16 +  
    1.17 +lemma (in real_normed_algebra_1) scaleR_power [simp]: 
    1.18 +  "(scaleR x y) ^ n = scaleR (x^n) (y^n)"
    1.19 +  by (induction n) (simp_all add: scaleR_one scaleR_scaleR mult_ac)
    1.20  
    1.21  class real_normed_div_algebra = real_div_algebra + real_normed_vector +
    1.22    assumes norm_mult: "norm (x * y) = norm x * norm y"