src/HOL/Set_Interval.thy
changeset 60017 b785d6d06430
parent 59416 fde2659085e1
child 60150 bd773c47ad0b
     1.1 --- a/src/HOL/Set_Interval.thy	Thu Apr 09 20:42:38 2015 +0200
     1.2 +++ b/src/HOL/Set_Interval.thy	Sat Apr 11 11:56:40 2015 +0100
     1.3 @@ -1562,12 +1562,6 @@
     1.4       "(\<Sum>i\<le>n. (\<Sum>j<i. a i j)) = (\<Sum>j<n. \<Sum>i = Suc j..n. a i j)"
     1.5    by (induction n) (auto simp: setsum.distrib)
     1.6  
     1.7 -lemma setsum_zero_power [simp]:
     1.8 -  fixes c :: "nat \<Rightarrow> 'a::division_ring"
     1.9 -  shows "(\<Sum>i\<in>A. c i * 0^i) = (if finite A \<and> 0 \<in> A then c 0 else 0)"
    1.10 -apply (cases "finite A")
    1.11 -  by (induction A rule: finite_induct) auto
    1.12 -
    1.13  lemma setsum_zero_power' [simp]:
    1.14    fixes c :: "nat \<Rightarrow> 'a::field"
    1.15    shows "(\<Sum>i\<in>A. c i * 0^i / d i) = (if finite A \<and> 0 \<in> A then c 0 / d 0 else 0)"