ext — Mathlib

English

Two Pell solutions are equal if and only if their x and y coordinates are equal.

Русский

Два решения Пелля равны тогда и тогда, когда их x и y координаты совпадают.

LaTeX

$$$$ \forall a,b \in Pell.Solution_1(d),\ a.x = b.x \land a.y = b.y \Rightarrow a = b. $$$$

Lean4

/-- Two solutions are equal if their `x` and `y` components are equal. -/
@[ext]
theorem ext {a b : Solution₁ d} (hx : a.x = b.x) (hy : a.y = b.y) : a = b :=
  Subtype.ext <| Zsqrtd.ext hx hy

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