| changeset 58889 | 5b7a9633cfa8 |
| parent 58841 | e16712bb1d41 |
| child 58917 | a3be9a47e2d7 |
| 58888:9537bf1c4853 | 58889:5b7a9633cfa8 |
|---|---|
2 Authors: Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow |
2 Authors: Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow |
3 |
3 |
4 Defines the "choose" function, and establishes basic properties. |
4 Defines the "choose" function, and establishes basic properties. |
5 *) |
5 *) |
6 |
6 |
7 header {* Binomial *} |
7 section {* Binomial *} |
8 |
8 |
9 theory Binomial |
9 theory Binomial |
10 imports Cong Fact Complex_Main |
10 imports Cong Fact Complex_Main |
11 begin |
11 begin |
12 |
12 |