re_pellZd

Mathlib.NumberTheory.PellMatiyasevic

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

English

The real part of pellZd(a1,n) is xn(a1,n).

Русский

Доля вещественная pellZd(a1,n) равна xn(a1,n).

LaTeX

$$$ (pellZd(a1, n)).re = xn(a1, n) $$$

Lean4

@[simp]
theorem re_pellZd (n : ℕ) : (pellZd a1 n).re = xn a1 n :=
  rfl

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

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

Разделы

Аффилиация

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