prop — Mathlib

English

For any Pell solution a = (x,y) in Pell.Solution₁ d, the Pell equation x^2 - d y^2 = 1 holds.

Русский

Для любого решения Пелля a = (x,y) в Pell.Solution₁ d выполняется тождество x^2 - d y^2 = 1.

LaTeX

$$$$ a.x^2 - d\, a.y^2 = 1. $$$$

Lean4

/-- The proof that `a` is a solution to the Pell equation `x^2 - d*y^2 = 1` -/
theorem prop (a : Solution₁ d) : a.x ^ 2 - d * a.y ^ 2 = 1 :=
  is_pell_solution_iff_mem_unitary.mpr a.property

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