sZMod_eq_sMod

Mathlib.NumberTheory.LucasLehmer

URI: https://scilib.ai/kg/mathlib#LucasLehmer.sZMod_eq_sMod

← MathLib Explorer

English

For every p and i, sZMod p i equals sMod p i considered as an element of ZMod (2^p − 1).

Русский

Для любых p и i, sZMod(p,i) равно sMod(p,i) в ZMod(2^p − 1).

LaTeX

$$sZMod p i = (sMod p i)\.cast$$

Lean4

theorem sZMod_eq_sMod (p : ℕ) (i : ℕ) : sZMod p i = (sMod p i : ZMod (2 ^ p - 1)) := by
  induction i <;> push_cast [← Int.coe_nat_two_pow_pred p, sMod, sZMod, *] <;> rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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