mk — Mathlib · SciLib

English

One can construct a Pell.Solution₁ d from an integer pair (x,y) and a proof that x^2 - d y^2 = 1.

Русский

Можно сконструировать Pell.Solution₁ d из целой пары (x,y) и доказательства того, что x^2 - d y^2 = 1.

LaTeX

$$$$ \forall x,y \in \mathbb{Z}, \forall prop:\; x^2 - d y^2 = 1, \mathrm{mk}(x,y,prop) \in Pell.Solution_1(d). $$$$

Lean4

/-- Construct a solution from `x`, `y` and a proof that the equation is satisfied. -/
def mk (x y : ℤ) (prop : x ^ 2 - d * y ^ 2 = 1) : Solution₁ d
    where
  val := ⟨x, y⟩
  property := is_pell_solution_iff_mem_unitary.mp prop

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