sModNat_aux

Mathlib.NumberTheory.LucasLehmer

URI: https://scilib.ai/kg/mathlib#LucasLehmer.norm_num_ext.sModNat_aux

Lean4

/-- Generalization of `sModNat` with arbitrary base case,
useful for proving `sModNatTR` and `sModNat` agree.
-/
def sModNat_aux (b q : ℕ) : ℕ → ℕ
  | 0 => b
  | i + 1 => (sModNat_aux b q i ^ 2 + (q - 2)) % q

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

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

Разделы

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

Аффилиация

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