English
A positive solution is a generator (up to sign) of the Pell group if and only if it is a fundamental solution.
Русский
Положительное решение является генератором группы решений Пелля (сверх знака) тогда и только тогда, когда оно является фундаментальным решением.
LaTeX
$$For all d, a ∈ Solution_1(d): (1 < a.x ∧ 0 < a.y ∧ ∀ b ∈ Solution_1(d), ∃ n ∈ ℤ, b = a^n ∨ b = -a^n) ↔ IsFundamental(a).$$
Lean4
/-- A positive solution is a generator (up to sign) of the group of all solutions to the
Pell equation `x^2 - d*y^2 = 1` if and only if it is a fundamental solution. -/
theorem pos_generator_iff_fundamental (a : Solution₁ d) :
(1 < a.x ∧ 0 < a.y ∧ ∀ b : Solution₁ d, ∃ n : ℤ, b = a ^ n ∨ b = -a ^ n) ↔ IsFundamental a :=
by
refine ⟨fun h => ?_, fun H => ⟨H.1, H.2.1, H.eq_zpow_or_neg_zpow⟩⟩
have h₀ := d_pos_of_one_lt_x h.1
have hd := d_nonsquare_of_one_lt_x h.1
obtain ⟨a₁, ha₁⟩ := IsFundamental.exists_of_not_isSquare h₀ hd
obtain ⟨b, -, hb₂⟩ := existsUnique_pos_generator h₀ hd
rwa [hb₂ a h, ← hb₂ a₁ ⟨ha₁.1, ha₁.2.1, ha₁.eq_zpow_or_neg_zpow⟩]
