--- 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