isNat_not_lucasLehmerTest — Mathlib

English

If p ≥ 3 and the Mersenne number M_p is prime, then Lucas–Lehmer test holds for p.

Русский

Если p ≥ 3 и число Мерсенна M_p простое, то тест Лукаса–Леммера для p выполняется.

LaTeX

$$$p \ge 3 \land \text{mersenne}(p) \text{ is prime} \Rightarrow \text{LucasLehmerTest } p$$$

Lean4

theorem isNat_not_lucasLehmerTest : {p np : ℕ} → IsNat p np → ¬LucasLehmerTest np → ¬LucasLehmerTest p
  | _, _, ⟨rfl⟩, h => h

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