xn_add — Mathlib

English

Let a > 1 and let x_n(a) and y_n(a) denote the Pell sequences associated to a. Then for all m, n ∈ ℕ,\n x(m+n) = x(m) x(n) + d(a) y(m) y(n).

Русский

Пусть a > 1 и пусть x_n(a) и y_n(a) обозначают последовательности Пелля, связанные с a. Тогда для всех m, n ∈ ℕ выполняется:\n x(m+n) = x(m) x(n) + d(a) y(m) y(n).

LaTeX

$$$x^{(a)}(m+n) = x^{(a)}(m)\\,x^{(a)}(n) + d(a)\\,y^{(a)}(m)\\,y^{(a)}(n),$$$

Lean4

theorem xn_add (m n) : xn a1 (m + n) = xn a1 m * xn a1 n + d a1 * yn a1 m * yn a1 n :=
  by
  injection pellZd_add a1 m n with h _
  zify
  rw [h]
  simp [pellZd]

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