src/HOL/Transcendental.thy
changeset 53599 78ea983f7987
parent 53079 ade63ccd6f4e
child 53602 0ae3db699a3e
     1.1 --- a/src/HOL/Transcendental.thy	Thu Sep 12 15:08:07 2013 -0700
     1.2 +++ b/src/HOL/Transcendental.thy	Thu Sep 12 15:08:46 2013 -0700
     1.3 @@ -57,7 +57,7 @@
     1.4    x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
     1.5  
     1.6  lemma powser_insidea:
     1.7 -  fixes x z :: "'a::real_normed_field"
     1.8 +  fixes x z :: "'a::real_normed_div_algebra"
     1.9    assumes 1: "summable (\<lambda>n. f n * x ^ n)"
    1.10      and 2: "norm z < norm x"
    1.11    shows "summable (\<lambda>n. norm (f n * z ^ n))"
    1.12 @@ -95,7 +95,7 @@
    1.13    proof -
    1.14      from 2 have "norm (norm (z * inverse x)) < 1"
    1.15        using x_neq_0
    1.16 -      by (simp add: nonzero_norm_divide divide_inverse [symmetric])
    1.17 +      by (simp add: norm_mult nonzero_norm_inverse divide_inverse [where 'a=real, symmetric])
    1.18      hence "summable (\<lambda>n. norm (z * inverse x) ^ n)"
    1.19        by (rule summable_geometric)
    1.20      hence "summable (\<lambda>n. K * norm (z * inverse x) ^ n)"
    1.21 @@ -110,7 +110,7 @@
    1.22  qed
    1.23  
    1.24  lemma powser_inside:
    1.25 -  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach}"
    1.26 +  fixes f :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
    1.27    shows
    1.28      "summable (\<lambda>n. f n * (x ^ n)) \<Longrightarrow> norm z < norm x \<Longrightarrow>
    1.29        summable (\<lambda>n. f n * (z ^ n))"