equal
deleted
inserted
replaced
4 Copyright 2000 University of Cambridge |
4 Copyright 2000 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 header {* Wilson's Theorem using a more abstract approach *} |
7 header {* Wilson's Theorem using a more abstract approach *} |
8 |
8 |
9 theory WilsonBij = BijectionRel + IntFact: |
9 theory WilsonBij imports BijectionRel IntFact begin |
10 |
10 |
11 text {* |
11 text {* |
12 Wilson's Theorem using a more ``abstract'' approach based on |
12 Wilson's Theorem using a more ``abstract'' approach based on |
13 bijections between sets. Does not use Fermat's Little Theorem |
13 bijections between sets. Does not use Fermat's Little Theorem |
14 (unlike Russinoff). |
14 (unlike Russinoff). |