exists_nontrivial_of_not_isSquare

English

If a fundamental Pell solution exists, it is unique.

Русский

Если существует фундаментальное решение Пелля, оно единственно.

LaTeX

$$$\forall a,b\in \mathrm{Solution}_1(d),\; \text{IsFundamental}(a) \land \text{IsFundamental}(b) \rightarrow a=b$$$

Lean4

/-- If `d` is a positive integer that is not a square, then there exists a nontrivial solution
to the Pell equation `x^2 - d*y^2 = 1`. -/
theorem exists_nontrivial_of_not_isSquare (h₀ : 0 < d) (hd : ¬IsSquare d) : ∃ a : Solution₁ d, a ≠ 1 ∧ a ≠ -1 :=
  by
  obtain ⟨x, y, prop, hy⟩ := exists_of_not_isSquare h₀ hd
  refine ⟨mk x y prop, fun H => ?_, fun H => ?_⟩ <;> apply_fun Solution₁.y at H <;> simp [hy] at H

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