ω_pow_eq_one — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem ω_pow_eq_one (p' : ℕ) (h : lucasLehmerResidue (p' + 2) = 0) : (ω : X (q (p' + 2))) ^ 2 ^ (p' + 2) = 1 :=
  calc
    (ω : X (q (p' + 2))) ^ 2 ^ (p' + 2) = (ω ^ 2 ^ (p' + 1)) ^ 2 := by rw [← pow_mul, ← Nat.pow_succ]
    _ = (-1) ^ 2 := by rw [ω_pow_eq_neg_one p' h]
    _ = 1 := by simp

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