lucasLehmerResidue — Mathlib

English

q(p) is defined as the minimum factor of M_p, packaged as a positive natural.

Русский

q(p) — это минимальный ненулевой делитель числа M_p, упакованный как положительное натуральное число.

LaTeX

$$q(p) = ⟨minFac (mersenne p), minFac_pos (mersenne p)⟩$$

Lean4

/-- The Lucas-Lehmer residue is `s p (p-2)` in `ZMod (2^p - 1)`. -/
def lucasLehmerResidue (p : ℕ) : ZMod (2 ^ p - 1) :=
  sZMod p (p - 2)

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