sModNatTR — Mathlib

English

The tail-recursive version sModNatTR agrees with sModNat: sModNatTR q i = sModNat q i.

Русский

Хвострекурсивная версия sModNatTR совпадает с sModNat: sModNatTR q i = sModNat q i.

LaTeX

$$$\forall q,i:\; \mathrm{sModNatTR}\,q\,i = \mathrm{sModNat}\,q\,i$$$

Lean4

/-- Tail-recursive version of `sModNat`. -/
def sModNatTR (q k : ℕ) : ℕ :=
  go k (4 % q)
where/-- Helper function for `sMod''`. -/
   go : ℕ → ℕ → ℕ
    | 0, acc => acc
    | n + 1, acc => go n ((acc ^ 2 + (q - 2)) % q)

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