lucas_lehmer_sufficiency — Mathlib

English

If the Lucas–Lehmer test holds for p, then the Mersenne number 2^p − 1 is prime.

Русский

Если тест Лукас–Леммера выполняется для p, то число Мерсенна 2^p − 1 простое.

LaTeX

$$$\text{LucasLehmerTest}(p) \Rightarrow \text{Prime}(\text{mersenne}(p))$$$

Lean4

theorem lucas_lehmer_sufficiency (p : ℕ) (w : 1 < p) : LucasLehmerTest p → (mersenne p).Prime :=
  by
  set p' := p - 2 with hp'
  clear_value p'
  obtain rfl : p = p' + 2 := by cutsat
  have w : 1 < p' + 2 := Nat.lt_of_sub_eq_succ rfl
  contrapose
  intro a t
  have h₁ := order_ineq p' t
  have h₂ := Nat.minFac_sq_le_self (mersenne_pos.2 (Nat.lt_of_succ_lt w)) a
  have h := lt_of_lt_of_le h₁ h₂
  exact not_lt_of_ge (Nat.sub_le _ _) h

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