pell_val

Mathlib.NumberTheory.PellMatiyasevic

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

← MathLib Explorer

English

The Pell function Pell(a1,n) returns the pair (x_n, y_n); Pell(a1,n) = (x_n, y_n).

Русский

Функция Pell(a1,n) возвращает пару (x_n, y_n); Pell(a1,n) = (x_n, y_n).

LaTeX

$$$\text{pell}(a_1,n) = (x_n,y_n).$$$

Lean4

@[simp]
theorem pell_val (n : ℕ) : pell a1 n = (xn a1 n, yn a1 n) :=
  show pell a1 n = ((pell a1 n).1, (pell a1 n).2) from
    match pell a1 n with
    | (_, _) => rfl

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

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

Разделы

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

Аффилиация

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