Wilson's theorem. #
This file contains a proof of Wilson's theorem.
The heavy lifting is mostly done by the previous wilsons_lemma
,
but here we also prove the other logical direction.
This could be generalized to similar results about finite abelian groups.
References #
TODO #
- Give
wilsons_lemma
a descriptive name.
@[simp]
Wilson's Lemma: the product of 1
, ..., p-1
is -1
modulo p
.
@[simp]
theorem
ZMod.prod_Ico_one_prime
(p : ℕ)
[Fact (Nat.Prime p)]
:
(Finset.prod (Finset.Ico 1 p) fun x => ↑x) = -1
For n ≠ 1
, (n-1)!
is congruent to -1
modulo n
only if n is prime.
Wilson's Theorem: For n ≠ 1
, (n-1)!
is congruent to -1
modulo n
iff n is prime.