equal
deleted
inserted
replaced
370 also have "phi p = nat p - 1" |
370 also have "phi p = nat p - 1" |
371 by (rule phi_prime, rule assms) |
371 by (rule phi_prime, rule assms) |
372 finally show ?thesis . |
372 finally show ?thesis . |
373 qed |
373 qed |
374 |
374 |
|
375 lemma fermat_theorem_nat: |
|
376 assumes "prime p" and "~ (p dvd a)" |
|
377 shows "[a^(p - 1) = 1] (mod p)" |
|
378 using fermat_theorem [of p a] assms |
|
379 by (metis int_1 nat_int of_nat_power prime_int_def transfer_int_nat_cong zdvd_int) |
|
380 |
375 |
381 |
376 subsection {* Wilson's theorem *} |
382 subsection {* Wilson's theorem *} |
377 |
383 |
378 lemma (in field) inv_pair_lemma: "x : Units R \<Longrightarrow> y : Units R \<Longrightarrow> |
384 lemma (in field) inv_pair_lemma: "x : Units R \<Longrightarrow> y : Units R \<Longrightarrow> |
379 {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}" |
385 {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}" |