isNat_lucasLehmerTest — Mathlib

English

If p > 1, and Lucas-Lehmer test holds for p, then the Mersenne number M_p is prime.

Русский

Если p > 1 и тест Лукаса-Леммера выполняется для p, тогда число Мерсенна M_p простое.

LaTeX

$$$p > 1 \Rightarrow [\text{LucasLehmerTest } p] \Rightarrow \text{mersenne}(p) \text{ is prime}$$$

Lean4

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

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