changeset 36349 | 39be26d1bc28 |
parent 35028 | 108662d50512 |
child 36409 | d323e7773aa8 |
--- a/src/HOL/Series.thy Mon Apr 26 11:34:15 2010 +0200 +++ b/src/HOL/Series.thy Mon Apr 26 11:34:17 2010 +0200 @@ -381,7 +381,7 @@ shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)" by (rule geometric_sums [THEN sums_summable]) -lemma half: "0 < 1 / (2::'a::{number_ring,division_by_zero,linordered_field})" +lemma half: "0 < 1 / (2::'a::{number_ring,division_ring_inverse_zero,linordered_field})" by arith lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1"