| changeset 21404 | eb85850d3eb7 |
| parent 19670 | 2e4a143c73c5 |
| child 23894 | 1a4167d761ac |
| 21403:dd58f13a8eb4 | 21404:eb85850d3eb7 |
|---|---|
14 *} |
14 *} |
15 |
15 |
16 subsection {* Definitions and lemmas *} |
16 subsection {* Definitions and lemmas *} |
17 |
17 |
18 definition |
18 definition |
19 inv :: "int => int => int" |
19 inv :: "int => int => int" where |
20 "inv p a = (a^(nat (p - 2))) mod p" |
20 "inv p a = (a^(nat (p - 2))) mod p" |
21 |
21 |
22 consts |
22 consts |
23 wset :: "int * int => int set" |
23 wset :: "int * int => int set" |
24 |
24 |