sZMod_eq_s — Mathlib

English

For all p and i, sZMod(p,i) equals s(i) reduced to the modulus 2^p − 1.

Русский

Для любых p и i, sZMod(p,i) равен s(i), приведённому по модулю 2^p − 1.

LaTeX

$$sZMod(p,i) = (s(i) : ZMod (2^p - 1))$$

Lean4

theorem sZMod_eq_s (p' : ℕ) (i : ℕ) : sZMod (p' + 2) i = (s i : ZMod (2 ^ (p' + 2) - 1)) := by
  induction i with
  | zero => dsimp [s, sZMod]; simp
  | succ i ih => push_cast [s, sZMod, ih];
    rfl
      -- These next two don't make good `norm_cast` lemmas.

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