x — Mathlib · SciLib

English

The x-coordinate of a Pell solution is the real part of its representation in Z[√d].

Русский

x-координата решения Пелля равна вещественной части его представления в Z[√d].

LaTeX

$$$$ a=(x,y) \in Pell.Solution_1(d) \implies a.x = x = \Re(a : \mathbb{Z}[\sqrt{d}]). $$$$

Lean4

/-- The `x` component of a solution to the Pell equation `x^2 - d*y^2 = 1` -/
protected def x (a : Solution₁ d) : ℤ :=
  (a : ℤ√d).re

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