equal
deleted
inserted
replaced
5 Copyright: Clemens Ballarin |
5 Copyright: Clemens Ballarin |
6 *) |
6 *) |
7 |
7 |
8 header {* Univariate Polynomials *} |
8 header {* Univariate Polynomials *} |
9 |
9 |
10 theory UnivPoly2 = Abstract: |
10 theory UnivPoly2 |
|
11 imports "../abstract/Abstract" |
|
12 begin |
11 |
13 |
12 (* already proved in Finite_Set.thy |
14 (* already proved in Finite_Set.thy |
13 |
15 |
14 lemma setsum_cong: |
16 lemma setsum_cong: |
15 "[| A = B; !!i. i : B ==> f i = g i |] ==> setsum f A = setsum g B" |
17 "[| A = B; !!i. i : B ==> f i = g i |] ==> setsum f A = setsum g B" |