src/HOL/Real_Vector_Spaces.thy
changeset 60762 bf0c76ccee8d
parent 60758 d8d85a8172b5
child 60800 7d04351c795a
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Mon Jul 20 11:40:43 2015 +0200
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Jul 20 23:12:50 2015 +0100
     1.3 @@ -862,6 +862,25 @@
     1.4    shows "norm (x ^ n) = norm x ^ n"
     1.5  by (induct n) (simp_all add: norm_mult)
     1.6  
     1.7 +lemma norm_mult_numeral1 [simp]:
     1.8 +  fixes a b :: "'a::{real_normed_field, field}"
     1.9 +  shows "norm (numeral w * a) = numeral w * norm a"
    1.10 +by (simp add: norm_mult)
    1.11 +
    1.12 +lemma norm_mult_numeral2 [simp]:
    1.13 +  fixes a b :: "'a::{real_normed_field, field}"
    1.14 +  shows "norm (a * numeral w) = norm a * numeral w"
    1.15 +by (simp add: norm_mult)
    1.16 +
    1.17 +lemma norm_divide_numeral [simp]:
    1.18 +  fixes a b :: "'a::{real_normed_field, field}"
    1.19 +  shows "norm (a / numeral w) = norm a / numeral w"
    1.20 +by (simp add: norm_divide)
    1.21 +
    1.22 +lemma norm_of_real_diff [simp]:
    1.23 +    "norm (of_real b - of_real a :: 'a::real_normed_algebra_1) \<le> \<bar>b - a\<bar>"
    1.24 +  by (metis norm_of_real of_real_diff order_refl)
    1.25 +
    1.26  text\<open>Despite a superficial resemblance, @{text norm_eq_1} is not relevant.\<close>
    1.27  lemma square_norm_one:
    1.28    fixes x :: "'a::real_normed_div_algebra"