pepin_primality' — Mathlib

English

F_n is prime if 3^{(F_n − 1)/2} ≡ −1 (mod F_n).

Русский

Число Ферма F_n простое, если 3^{(F_n−1)/2} ≡ −1 (mod F_n).

LaTeX

$$3^{(\\mathrm{fermatNumber}(n) - 1)/2} \\equiv -1 \\pmod{\\mathrm{fermatNumber}(n)}$$

Lean4

/-- `Fₙ = 2^(2^n)+1` is prime if `3^((Fₙ - 1)/2) = -1 mod Fₙ` (**Pépin's test**). -/
theorem pepin_primality' (n : ℕ) (h : 3 ^ ((fermatNumber n - 1) / 2) = (-1 : ZMod (fermatNumber n))) :
    (fermatNumber n).Prime := by
  apply pepin_primality
  rw [← h]
  congr
  rw [fermatNumber, add_tsub_cancel_right, Nat.pow_div Nat.one_le_two_pow Nat.zero_lt_two]

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