equal
deleted
inserted
replaced
6 header {*Integers: Divisibility and Congruences*} |
6 header {*Integers: Divisibility and Congruences*} |
7 |
7 |
8 theory Int2 imports Finite2 WilsonRuss begin |
8 theory Int2 imports Finite2 WilsonRuss begin |
9 |
9 |
10 definition |
10 definition |
11 MultInv :: "int => int => int" |
11 MultInv :: "int => int => int" where |
12 "MultInv p x = x ^ nat (p - 2)" |
12 "MultInv p x = x ^ nat (p - 2)" |
13 |
13 |
14 |
14 |
15 subsection {* Useful lemmas about dvd and powers *} |
15 subsection {* Useful lemmas about dvd and powers *} |
16 |
16 |