# mathlibdocumentation

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.

## TODO #

• Move wilsons_lemma into this file, and give it a descriptive name.
theorem nat.prime_of_fac_equiv_neg_one {n : } (h : ((n - 1).factorial) = -1) (h1 : n 1) :

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) :
((n - 1).factorial) = -1

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