instDecidableEq

Mathlib.NumberTheory.LucasLehmer

URI: https://scilib.ai/kg/mathlib#LucasLehmer.X.instDecidableEq

English

For all p and i, sZMod(p,i) equals s(i) interpreted in ZMod (2^p − 1).

Русский

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

LaTeX

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

Lean4

instance : DecidableEq (X q) :=
  inferInstanceAs (DecidableEq (ZMod q × ZMod q))

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru