author | wenzelm |
Fri, 06 Apr 2012 12:45:56 +0200 | |
changeset 47382 | 5b902eeb2a29 |
parent 47381 | 376b91cdfea8 |
child 47383 | 003189cebf12 |
--- a/src/HOL/Library/Polynomial.thy Fri Apr 06 12:10:50 2012 +0200 +++ b/src/HOL/Library/Polynomial.thy Fri Apr 06 12:45:56 2012 +0200 @@ -492,7 +492,7 @@ subsection {* Multiplication of polynomials *} -text {* TODO: move to Set_Interval.thy *} +(* TODO: move to Set_Interval.thy *) lemma setsum_atMost_Suc_shift: fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add" shows "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"