IsPell — Mathlib

English

A predicate IsPell on elements of ℤ√d is defined by IsPell(⟨x,y⟩) if and only if x^2 − d y^2 = 1.

Русский

Для элемента ⟨x,y⟩ из кольца ℤ√d предикат IsPell определяется так: IsPell(⟨x,y⟩) тогда и только если x^2 − d y^2 = 1.

LaTeX

$$$\text{IsPell}(\langle x,y\rangle) \iff x^{2} - d y^{2} = 1.$$$

Lean4

/-- The property of being a solution to the Pell equation, expressed
  as a property of elements of `ℤ√d`. -/
def IsPell : ℤ√d → Prop
  | ⟨x, y⟩ => x * x - d * y * y = 1

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