Wilsons_Theorem
Provedfactorialnumber-theoryprimesproofwiki
A positive integer p is prime iff (p-1)! = -1 (mod p).
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Data.Nat.Prime.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic import Mathlib.Data.Nat.Prime.Basic theorem Wilsons_Theorem (p : ℕ) (hp : Nat.Prime p) : (Nat.factorial (p - 1)) % p = p - 1 := by sorry
Source