s

Mathlib.NumberTheory.LucasLehmer

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

English

Define a sequence s by s(0) = 4 and s(i+1) = (s(i))^2 − 2 in the integers.

Русский

Определим последовательность s следующeй формулой: s(0) = 4 и s(i+1) = (s(i))^2 − 2 по целым числам.

LaTeX

$$$s(0)=4,\qquad s(i+1)=s(i)^2-2\quad(\text{in } \mathbb{Z})$$$

Lean4

/-- The recurrence `s (i+1) = (s i)^2 - 2` in `ℤ`. -/
def s : ℕ → ℤ
  | 0 => 4
  | i + 1 => s i ^ 2 - 2

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

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

Разделы

Аффилиация

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