sMod_mod

Mathlib.NumberTheory.LucasLehmer

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

English

For any p, i, sMod(p,i) is congruent to itself modulo 2^p − 1.

Русский

Для любых p и i произведение sMod(p,i) эквивалентно себе по модулю 2^p − 1.

LaTeX

$$sMod(p,i) \equiv sMod(p,i) \pmod{2^p-1}$$

Lean4

theorem sMod_mod (p i : ℕ) : sMod p i % (2 ^ p - 1) = sMod p i := by cases i <;> simp [sMod]

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

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

Разделы

Аффилиация

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