xz_succ_succ

Mathlib.NumberTheory.PellMatiyasevic

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

← MathLib Explorer

English

For a > 1 and n, xz(a, n+2) = 2 a xz(a, n+1) − xz(a, n).

Русский

Для a > 1 и n выполняется: xz(n+2) = 2 a xz(n+1) − xz(n).

LaTeX

$$$x^{(a)}_{n+2} = 2 a\\; x^{(a)}_{n+1} - x^{(a)}_{n}$$$

Lean4

theorem xz_succ_succ (n) : xz a1 (n + 2) = (2 * a : ℕ) * xz a1 (n + 1) - xz a1 n :=
  eq_sub_of_add_eq <| by delta xz; rw [← Int.natCast_add, ← Int.natCast_mul, xn_succ_succ]

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

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

Разделы

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

Аффилиация

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