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.

Main results

• ZMod.wilsons_lemma: the value of (p - 1)! modulo a prime p.
• Nat.prime_iff_fac_equiv_neg_one: that value characterises primality.
• ZMod.factorial_eq_neg_one_pow_mul_half_factorial_sq expresses (p - 1)! using the square of the half-factorial when p is odd.
• ZMod.half_factorial_sq_eq_neg_one gives the half-factorial as an explicit square root of -1 modulo a prime not congruent to three modulo four.

References

• Wilson's Theorem

TODO

• Give wilsons_lemma a descriptive name.

theorem ZMod.factorial_eq_neg_one_pow_mul_half_factorial_sq {p : ℕ} (hp : Odd p) : ↑(p - 1).factorial = (-1) ^ ((p - 1) / 2) * ↑((p - 1) / 2).factorial ^ 2

If p is odd, pairing each factor above (p - 1) / 2 with its negative gives (p - 1)! = (-1) ^ ((p - 1) / 2) * (((p - 1) / 2)!) ^ 2 in ZMod p.

@[simp]

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

Wilson's Lemma: the product of 1, ..., p-1 is -1 modulo p.

theorem ZMod.half_factorial_sq_eq_neg_one {p : ℕ} [Fact (Nat.Prime p)] (hp : p % 4 ≠ 3) : ↑((p - 1) / 2).factorial ^ 2 = -1

Let p be prime with p % 4 ≠ 3. Then ((p - 1) / 2)! is a specified square root of -1 in ZMod p.

@[simp]

theorem ZMod.prod_Ico_one_prime (p : ℕ) [Fact (Nat.Prime p)] : ∏ x ∈ Finset.Ico 1 p, ↑x = -1

theorem Nat.prime_of_fac_equiv_neg_one {n : ℕ} (h : ↑(n - 1).factorial = -1) (h1 : n ≠ 1) : 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) : Prime n ↔ ↑(n - 1).factorial = -1

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