English
Wilson's lemma: for a prime p, the product (p−1)! is congruent to −1 modulo p.
Русский
Лемма Вильсона: для простого p произведение (p−1)! по модулю p равно −1.
LaTeX
$$$$ ((p-1)!) \\equiv -1 \\pmod{p}. $$$$
Lean4
/-- **Wilson's Lemma**: the product of `1`, ..., `p-1` is `-1` modulo `p`. -/
@[simp]
theorem wilsons_lemma : ((p - 1)! : ZMod p) = -1 :=
by
refine
calc
((p - 1)! : ZMod p) = ∏ x ∈ Ico 1 (succ (p - 1)), (x : ZMod p) := by
rw [← Finset.prod_Ico_id_eq_factorial, prod_natCast]
_ = ∏ x : (ZMod p)ˣ, (x : ZMod p) := ?_
_ = -1 := by
simp_rw [← Units.coeHom_apply, ← map_prod (Units.coeHom (ZMod p)), prod_univ_units_id_eq_neg_one,
Units.coeHom_apply, Units.val_neg, Units.val_one]
have hp : 0 < p := (Fact.out (p := p.Prime)).pos
symm
refine prod_bij (fun a _ => (a : ZMod p).val) ?_ ?_ ?_ ?_
· intro a ha
rw [mem_Ico, ← Nat.succ_sub hp, Nat.add_one_sub_one]
constructor
· apply Nat.pos_of_ne_zero; rw [← @val_zero p]
intro h; apply Units.ne_zero a (val_injective p h)
· exact val_lt _
· intro _ _ _ _ h; rw [Units.ext_iff]; exact val_injective p h
· intro b hb
rw [mem_Ico, Nat.succ_le_iff, ← succ_sub hp, Nat.add_one_sub_one, pos_iff_ne_zero] at hb
refine ⟨Units.mk0 b ?_, Finset.mem_univ _, ?_⟩
· intro h; apply hb.1; apply_fun val at h
simpa only [val_cast_of_lt hb.right, val_zero] using h
· simp only [val_cast_of_lt hb.right, Units.val_mk0]
· rintro a -; simp only [cast_id, natCast_val]
