# HG changeset patch
# User huffman
# Date 1158959859 -7200
# Node ID 74e8b46abb97376e4c3742e6b079a6b69a089bdc
# Parent  3d07617c8bf3edb0177f3d7ee46c4ff9d32214c5
add lemma norm_power

diff -r 3d07617c8bf3 -r 74e8b46abb97 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Fri Sep 22 21:42:12 2006 +0200
+++ b/src/HOL/Real/RealVector.thy	Fri Sep 22 23:17:39 2006 +0200
@@ -6,7 +6,7 @@
 header {* Vector Spaces and Algebras over the Reals *}
 
 theory RealVector
-imports RealDef
+imports RealPow
 begin
 
 subsection {* Locale for additive functions *}
@@ -489,4 +489,9 @@
   shows "norm (a / b) = norm a / norm b"
 by (simp add: divide_inverse norm_mult norm_inverse)
 
+lemma norm_power:
+  fixes x :: "'a::{real_normed_div_algebra,recpower}"
+  shows "norm (x ^ n) = norm x ^ n"
+by (induct n, simp, simp add: power_Suc norm_mult)
+
 end