| changeset 15140 | 322485b816ac |
| parent 15131 | c69542757a4d |
| child 15251 | bb6f072c8d10 |
| 15139:58cd3404cf75 | 15140:322485b816ac |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header{*Finite Summation and Infinite Series for Complex Numbers*} |
6 header{*Finite Summation and Infinite Series for Complex Numbers*} |
7 |
7 |
8 theory CSeries |
8 theory CSeries |
9 import CStar |
9 imports CStar |
10 begin |
10 begin |
11 |
11 |
12 consts sumc :: "[nat,nat,(nat=>complex)] => complex" |
12 consts sumc :: "[nat,nat,(nat=>complex)] => complex" |
13 primrec |
13 primrec |
14 sumc_0: "sumc m 0 f = 0" |
14 sumc_0: "sumc m 0 f = 0" |