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

• Wilson's Theorem

TODO

• Give wilsons_lemma a descriptive name.

@[simp]

theorem ZMod.wilsons_lemma (p : ℕ) [Fact (Nat.Prime p)] : ↑(Nat.factorial (p - 1)) = -1

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

theorem Nat.prime_of_fac_equiv_neg_one {n : ℕ} (h : ↑(Nat.factorial (n - 1)) = -1) (h1 : n ≠ 1) : Nat.Prime n

For n ≠ 1, (n-1)! is congruent to -1 modulo n only if n is prime.

theorem Nat.prime_iff_fac_equiv_neg_one {n : ℕ} (h : n ≠ 1) : Nat.Prime n ↔ ↑(Nat.factorial (n - 1)) = -1

Wilson's Theorem: For n ≠ 1, (n-1)! is congruent to -1 modulo n iff n is prime.