| changeset 35762 | af3ff2ba4c54 |
| parent 16417 | 9bc16273c2d4 |
| child 41777 | 1f7cbe39d425 |
| 35761:c4a698ee83b4 | 35762:af3ff2ba4c54 |
|---|---|
1 (* Title: ZF/ex/Natsum.thy |
1 (* Title: ZF/ex/Natsum.thy |
2 ID: $Id$ |
|
3 Author: Tobias Nipkow & Lawrence C Paulson |
2 Author: Tobias Nipkow & Lawrence C Paulson |
4 |
3 |
5 A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n. |
4 A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n. |
6 |
5 |
7 Note: n is a natural number but the sum is an integer, |
6 Note: n is a natural number but the sum is an integer, |