isPell_pellZd

Mathlib.NumberTheory.PellMatiyasevic

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

← MathLib Explorer

English

For every n, IsPell pellZd(a1,n) holds.

Русский

Для каждого n верно IsPell pellZd(a1,n).

LaTeX

$$$ \forall n:\, IsPell( pellZd(a1, n) ) $$$

Lean4

theorem isPell_pellZd : ∀ n : ℕ, IsPell (pellZd a1 n)
  | 0 => rfl
  | n + 1 => by
    let o := isPell_one a1
    simpa using Pell.isPell_mul (isPell_pellZd n) o

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

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

Разделы

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

Аффилиация

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