equal
deleted
inserted
replaced
853 |
853 |
854 subsection {* The formula for geometric sums *} |
854 subsection {* The formula for geometric sums *} |
855 |
855 |
856 lemma geometric_sum: |
856 lemma geometric_sum: |
857 "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) = |
857 "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) = |
858 (x ^ n - 1) / (x - 1::'a::{field, recpower})" |
858 (x ^ n - 1) / (x - 1::'a::{field})" |
859 by (induct "n") (simp_all add:field_simps power_Suc) |
859 by (induct "n") (simp_all add:field_simps power_Suc) |
860 |
860 |
861 subsection {* The formula for arithmetic sums *} |
861 subsection {* The formula for arithmetic sums *} |
862 |
862 |
863 lemma gauss_sum: |
863 lemma gauss_sum: |