# HG changeset patch # User huffman # Date 1379023726 25200 # Node ID 78ea983f79875ee36343f2107fb4d9524eb69417 # Parent 2bd8d459ebaea36343213e161877ef78de28b55a generalize lemmas diff -r 2bd8d459ebae -r 78ea983f7987 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Thu Sep 12 15:08:07 2013 -0700 +++ b/src/HOL/Transcendental.thy Thu Sep 12 15:08:46 2013 -0700 @@ -57,7 +57,7 @@ x}, then it sums absolutely for @{term z} with @{term "\z\ < \x\"}.*} lemma powser_insidea: - fixes x z :: "'a::real_normed_field" + fixes x z :: "'a::real_normed_div_algebra" assumes 1: "summable (\n. f n * x ^ n)" and 2: "norm z < norm x" shows "summable (\n. norm (f n * z ^ n))" @@ -95,7 +95,7 @@ proof - from 2 have "norm (norm (z * inverse x)) < 1" using x_neq_0 - by (simp add: nonzero_norm_divide divide_inverse [symmetric]) + by (simp add: norm_mult nonzero_norm_inverse divide_inverse [where 'a=real, symmetric]) hence "summable (\n. norm (z * inverse x) ^ n)" by (rule summable_geometric) hence "summable (\n. K * norm (z * inverse x) ^ n)" @@ -110,7 +110,7 @@ qed lemma powser_inside: - fixes f :: "nat \ 'a::{real_normed_field,banach}" + fixes f :: "nat \ 'a::{real_normed_div_algebra,banach}" shows "summable (\n. f n * (x ^ n)) \ norm z < norm x \ summable (\n. f n * (z ^ n))"