# HG changeset patch # User nipkow # Date 1503505736 -7200 # Node ID cc66ab2373ce87fe32b3a8610d8dff2fbaf06efc # Parent 495df623251763a83d15e86c3c5d75c2513f07df added lemma diff -r 495df6232517 -r cc66ab2373ce src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Wed Aug 23 14:37:22 2017 +0200 +++ b/src/HOL/Set_Interval.thy Wed Aug 23 18:28:56 2017 +0200 @@ -1894,6 +1894,9 @@ subsection \The formula for geometric sums\ +lemma sum_power2: "(\i=0.. 1" shows "(\i