ω_pow_eq_neg_one — Mathlib

English

If Lucas–Lehmer residue at p' + 2 is zero, then ω^{2^{p' + 1}} = −1.

Русский

Если остаток Лукаса–Леммера при p' + 2 равен нулю, то ω^{2^{p' + 1}} = −1.

LaTeX

$$$\operatorname{lucasLehmerResidue}(p'+2) = 0 \Rightarrow (\omega : X (q (p'+2)))^{2^{p'+1}} = -1.$$$

Lean4

theorem ω_pow_eq_neg_one (p' : ℕ) (h : lucasLehmerResidue (p' + 2) = 0) : (ω : X (q (p' + 2))) ^ 2 ^ (p' + 1) = -1 :=
  by
  obtain ⟨k, w⟩ := ω_pow_formula p' h
  rw [mersenne_coe_X] at w
  simpa using w

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