pell — Mathlib

English

The x-coordinate sequence x_n is defined by x_n = (pell(a1,n)).1 with a1 > 1.

Русский

Последовательность x-координат Пелля задаётся как x_n = первый компонент пары Pell(a1,n) при a1 > 1.

LaTeX

$$$x_n = (\text{pell}(a_1,n))_{1},\quad a_1>1.$$$

Lean4

/-- The Pell sequences, i.e. the sequence of integer solutions to `x ^ 2 - d * y ^ 2 = 1`, where
`d = a ^ 2 - 1`, defined together in mutual recursion. -/
--@[nolint dup_namespace]

def pell : ℕ → ℕ × ℕ
  | 0 => (1, 0)
  | n + 1 => ((pell n).1 * a + d a1 * (pell n).2, (pell n).1 + (pell n).2 * a)

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