testTrueHelper — Mathlib

English

Given p and a witness to a certain residue condition, one can deduce Lucas-Lehmer test value for p.

Русский

Для данного p и условия остатка можно вывести значение теста Лукaс-Леммера для p.

LaTeX

$$$\text{testTrueHelper}(p)\Rightarrow \text{LucasLehmerTest}(p)$$$

Lean4

theorem testTrueHelper (p : ℕ) (hp : Nat.blt 1 p = true) (h : sModNatTR (2 ^ p - 1) (p - 2) = 0) : LucasLehmerTest p :=
  by
  rw [Nat.blt_eq] at hp
  rw [LucasLehmerTest, LucasLehmer.residue_eq_zero_iff_sMod_eq_zero p hp, ← sModNat_eq_sMod p _ hp, ←
    sModNatTR_eq_sModNat, h]
  rfl

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