eq_one_of_x_eq_one — Mathlib

English

Let d be nonzero. If a is a Pell solution with x-coordinate equal to 1, then a is the trivial solution (1, 0).

Русский

Пусть d ≠ 0. Если решение Пелля имеет x = 1, то оно тривиально: (1, 0).

LaTeX

$$$\forall d\in \mathbb{Z}, d \neq 0\;\forall a\in \mathrm{Solution}_1(d),\; a_x = 1 \rightarrow a = 1$$$

Lean4

/-- A solution with `x = 1` is trivial. -/
theorem eq_one_of_x_eq_one (h₀ : d ≠ 0) {a : Solution₁ d} (ha : a.x = 1) : a = 1 :=
  by
  have prop := a.prop_y
  rw [ha, one_pow, sub_self, mul_eq_zero, or_iff_right h₀, sq_eq_zero_iff] at prop
  exact ext ha prop

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