equal
deleted
inserted
replaced
342 apply (simp (no_asm)) |
342 apply (simp (no_asm)) |
343 apply (rule_tac x = "2" in exI) |
343 apply (rule_tac x = "2" in exI) |
344 apply safe |
344 apply safe |
345 apply (rule_tac x = "2" in exI) |
345 apply (rule_tac x = "2" in exI) |
346 apply auto |
346 apply auto |
347 apply arith |
|
348 done |
347 done |
349 |
348 |
350 theorem Wilson_Russ: |
349 theorem Wilson_Russ: |
351 "p \<in> zprime ==> [zfact (p - 1) = -1] (mod p)" |
350 "p \<in> zprime ==> [zfact (p - 1) = -1] (mod p)" |
352 apply (subgoal_tac "[(p - 1) * zfact (p - 2) = -1 * 1] (mod p)") |
351 apply (subgoal_tac "[(p - 1) * zfact (p - 2) = -1 * 1] (mod p)") |