equal
deleted
inserted
replaced
7 repaired proof of Bnor_prime (removed use of zprime_def) |
7 repaired proof of Bnor_prime (removed use of zprime_def) |
8 *) |
8 *) |
9 |
9 |
10 header {* Fermat's Little Theorem extended to Euler's Totient function *} |
10 header {* Fermat's Little Theorem extended to Euler's Totient function *} |
11 |
11 |
12 theory EulerFermat = BijectionRel + IntFact: |
12 theory EulerFermat imports BijectionRel IntFact begin |
13 |
13 |
14 text {* |
14 text {* |
15 Fermat's Little Theorem extended to Euler's Totient function. More |
15 Fermat's Little Theorem extended to Euler's Totient function. More |
16 abstract approach than Boyer-Moore (which seems necessary to achieve |
16 abstract approach than Boyer-Moore (which seems necessary to achieve |
17 the extended version). |
17 the extended version). |