yz_succ

Mathlib.NumberTheory.PellMatiyasevic

URI: https://scilib.ai/kg/mathlib#Pell.yz_succ

English

The yz-sequence satisfies the recurrence yz(a1, n+1) = xz(a1, n) + yz(a1, n)·az(a).

Русский

Для последовательности yz выполняется yz(a1, n+1) = xz(a1, n) + yz(a1, n)·az(a).

LaTeX

$$$ yz(a1, n+1) = xz(a1, n) + yz(a1, n) \cdot az(a) $$$

Lean4

@[simp]
theorem yz_succ (n : ℕ) : yz a1 (n + 1) = xz a1 n + yz a1 n * az a :=
  rfl

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

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

Разделы

Аффилиация

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