mathlib documentation

number_theory.wilson

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 #

source
theorem nat.prime_of_fac_equiv_neg_one {n : ℕ} (h : ↑((n - 1).factorial) = -1) (h1 : n ≠ 1) :
nat.prime n

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

source
theorem nat.prime_iff_fac_equiv_neg_one {n : ℕ} (h : n ≠ 1) :
nat.prime n ↔ ↑((n - 1).factorial) = -1

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