xn_succ

Mathlib.NumberTheory.PellMatiyasevic

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

English

The recurrence for x_{n+1} is x_{n+1} = x_n a + d(a_1) y_n.

Русский

Рекуррентность: x_{n+1} = x_n a + d(a_1) y_n.

LaTeX

$$$x_{n+1} = x_n \cdot a + d(a_1) \cdot y_n.$$$

Lean4

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

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

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

Разделы

Аффилиация

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