isPell_one

Mathlib.NumberTheory.PellMatiyasevic

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

English

The element ⟨a,1⟩ lies in the Pell set: IsPell(⟨a,1⟩).

Русский

Элемент ⟨a,1⟩ принадлежит сетке Пелля: IsPell(⟨a,1⟩).

LaTeX

$$$ IsPell(\langle a, 1 \rangle) $$$

Lean4

theorem isPell_one : IsPell (⟨a, 1⟩ : ℤ√(d a1)) :=
  show az a * az a - d a1 * 1 * 1 = 1 by simp [dz_val]

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

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

Разделы

Аффилиация

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