yn_add — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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