pellZd — Mathlib

English

The Pell sequence can also be viewed as an element of ℤ√d: pellZd(n) = ⟨xn(a1,n), yn(a1,n)⟩.

Русский

Последовательность Пелля может рассматриваться как элемент ℤ√d: pellZd(n) = ⟨x_n(a1,n), y_n(a1,n)⟩.

LaTeX

$$$ pellZd(a1, n) = \langle xn(a1, n), yn(a1, n) \rangle $$$

Lean4

/-- The Pell sequence can also be viewed as an element of `ℤ√d` -/
def pellZd (n : ℕ) : ℤ√(d a1) :=
  ⟨xn a1 n, yn a1 n⟩

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