| changeset 31017 | 2c227493ea56 |
| parent 30384 | 2f24531b2d3e |
| child 31044 | 6896c2498ac0 |
--- a/src/HOL/SetInterval.thy Tue Apr 28 15:50:30 2009 +0200 +++ b/src/HOL/SetInterval.thy Tue Apr 28 15:50:30 2009 +0200 @@ -855,7 +855,7 @@ lemma geometric_sum: "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) = - (x ^ n - 1) / (x - 1::'a::{field, recpower})" + (x ^ n - 1) / (x - 1::'a::{field})" by (induct "n") (simp_all add:field_simps power_Suc) subsection {* The formula for arithmetic sums *}