English
For d ∈ ℤ and a ∈ ℤ√d, the Pell equation a.re^2 − d a.im^2 = 1 holds if and only if a lies in the unitary submonoid of ℤ√d.
Русский
Для d ∈ ℤ и a ∈ ℤ√d, уравнение Пелля a.re^2 − d a.im^2 = 1 имеет решение тогда и только тогда, когда a лежит в подмоноиде unitary ℤ√d.
LaTeX
$$$a.re^2 - d \\cdot a.im^2 = 1 \\quad\\iff\\quad a \\in unitary(\\mathbb{Z}\\sqrt{d})$$$
Lean4
/-- An element of `ℤ√d` has norm one (i.e., `a.re^2 - d*a.im^2 = 1`) if and only if
it is contained in the submonoid of unitary elements.
TODO: merge this result with `Pell.isPell_iff_mem_unitary`. -/
theorem is_pell_solution_iff_mem_unitary {d : ℤ} {a : ℤ√d} : a.re ^ 2 - d * a.im ^ 2 = 1 ↔ a ∈ unitary (ℤ√d) := by
rw [← norm_eq_one_iff_mem_unitary, norm_def, sq, sq, ← mul_assoc]
-- We use `solution₁ d` to allow for a more general structure `solution d m` that
-- encodes solutions to `x^2 - d*y^2 = m` to be added later.
