yn_succ

Mathlib.NumberTheory.PellMatiyasevic

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

English

The recurrence for y_{n+1} is y_{n+1} = x_n + a y_n.

Русский

Рекуррентность: y_{n+1} = x_n + a y_n.

LaTeX

$$$y_{n+1} = x_n + a \cdot y_n.$$$

Lean4

@[simp]
theorem yn_succ (n : ℕ) : yn a1 (n + 1) = xn a1 n + yn a1 n * a :=
  rfl

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

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

Разделы

Аффилиация

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