sModNat — Mathlib

English

For p,k, with hp: 2 ≤ p, we have that the integer sModNat(2^p−1) k equals sMod p k.

Русский

Для p,k, при hp: 2 ≤ p, имеет место равенство числа sModNat(2^p−1) k и sMod p k в целых.

LaTeX

$$$ (sModNat (2^p - 1) k : \\mathbb{Z}) = sMod\; p\; k \\quad \\text{for } hp:\\, 2 \\le p $$$

Lean4

/-- Version of `sMod` that is `ℕ`-valued. One should have `q = 2 ^ p - 1`.
This can be reduced by the kernel. -/
def sModNat (q : ℕ) : ℕ → ℕ
  | 0 => 4 % q
  | i + 1 => (sModNat q i ^ 2 + (q - 2)) % q

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