yn_one

Mathlib.NumberTheory.PellMatiyasevic

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

English

Let a be a natural number with a > 1. Then the Pell y-sequence has its first term equal to 1: y_1 = 1.

Русский

Пусть a ∈ ℕ и a > 1. Тогда в последовательности Пелля для y первый член равен 1: y_1 = 1.

LaTeX

$$$ yn(a1, 1) = 1 $$$

Lean4

theorem yn_one : yn a1 1 = 1 := by simp

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

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

Разделы

Аффилиация

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