y — Mathlib · SciLib

English

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

Русский

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

LaTeX

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

Lean4

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

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