equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Vector Spaces and Algebras over the Reals *} |
6 header {* Vector Spaces and Algebras over the Reals *} |
7 |
7 |
8 theory RealVector |
8 theory RealVector |
9 imports RealDef |
9 imports RealPow |
10 begin |
10 begin |
11 |
11 |
12 subsection {* Locale for additive functions *} |
12 subsection {* Locale for additive functions *} |
13 |
13 |
14 locale additive = |
14 locale additive = |
487 lemma norm_divide: |
487 lemma norm_divide: |
488 fixes a b :: "'a::{real_normed_field,division_by_zero}" |
488 fixes a b :: "'a::{real_normed_field,division_by_zero}" |
489 shows "norm (a / b) = norm a / norm b" |
489 shows "norm (a / b) = norm a / norm b" |
490 by (simp add: divide_inverse norm_mult norm_inverse) |
490 by (simp add: divide_inverse norm_mult norm_inverse) |
491 |
491 |
|
492 lemma norm_power: |
|
493 fixes x :: "'a::{real_normed_div_algebra,recpower}" |
|
494 shows "norm (x ^ n) = norm x ^ n" |
|
495 by (induct n, simp, simp add: power_Suc norm_mult) |
|
496 |
492 end |
497 end |