prime_iff_fac_equiv_neg_one — Mathlib

English

For n ≠ 1, n is prime iff (n−1)! ≡ −1 (mod n).

Русский

Для n ≠ 1 число n простое тогда и только тогда, когда (n−1)! ≡ −1 (mod n).

LaTeX

$$$$ \\text{Prime}(n) \\;\\Longleftrightarrow\\; (n-1)! \\equiv -1 \\pmod{n} \\quad (n \\ne 1). $$$$

Lean4

/-- **Wilson's Theorem**: For `n ≠ 1`, `(n-1)!` is congruent to `-1` modulo `n` iff n is prime. -/
theorem prime_iff_fac_equiv_neg_one (h : n ≠ 1) : Prime n ↔ ((n - 1)! : ZMod n) = -1 :=
  by
  refine ⟨fun h1 => ?_, fun h2 => prime_of_fac_equiv_neg_one h2 h⟩
  haveI := Fact.mk h1
  exact ZMod.wilsons_lemma n

Похожие утверждения