LucasLehmerTest — Mathlib

English

**Lucas-Lehmer Test**: a Mersenne number is prime if and only if the Lucas-Lehmer residue is zero.

Русский

**Тест Лукaса-Лемерра**: число Мерсенна простое тогда и только тогда, когда остаток Лукaса-Лемерра равен нулю.

LaTeX

$$lucasLehmerResidue p = 0$$

Lean4

/-- **Lucas-Lehmer Test**: a Mersenne number `2^p-1` is prime if and only if
the Lucas-Lehmer residue `s p (p-2) % (2^p - 1)` is zero.
-/
def LucasLehmerTest (p : ℕ) : Prop :=
  lucasLehmerResidue p = 0

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