sZMod — Mathlib

English

Define sZMod(p) by sZMod(p,0) = 4 and sZMod(p,i+1) = (sZMod(p,i))^2 − 2 in ZMod(2^p − 1).

Русский

Определим sZMod(p) по аналогии в ZMod(2^p−1): sZMod(p,0)=4 и sZMod(p,i+1)=(sZMod(p,i))^2−2.

LaTeX

$$sZMod(p,0)=4,\quad sZMod(p,i+1)=sZMod(p,i)^2-2 \in \mathbb{Z}/(2^p-1)\mathbb{Z}$$

Lean4

/-- The recurrence `s (i+1) = (s i)^2 - 2` in `ZMod (2^p - 1)`. -/
def sZMod (p : ℕ) : ℕ → ZMod (2 ^ p - 1)
  | 0 => 4
  | i + 1 => sZMod p i ^ 2 - 2

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