English
Every Pell solution is, up to sign, a power of a given fundamental solution. More precisely, for a fixed fundamental a1, there exists n ∈ ℤ such that a = a1^n or a = -a1^n.
Русский
Каждое решение Пелля, кроме знака, является степенью данного фундаментального решения: существует n ∈ ℤ, такое что a = a1^n или a = -a1^n.
LaTeX
$$$\forall d \in \mathbb{Z},\; \forall a_1 \in \text{Solution}_1(d),\; \text{IsFundamental}(a_1) \Rightarrow \forall a \in \text{Solution}(d),\; \exists n \in \mathbb{Z},\; a = a_1^{n} \lor a = -a_1^{n}.$$$
Lean4
/-- Every solution is, up to a sign, a power of a given fundamental solution. -/
theorem eq_zpow_or_neg_zpow {a₁ : Solution₁ d} (h : IsFundamental a₁) (a : Solution₁ d) :
∃ n : ℤ, a = a₁ ^ n ∨ a = -a₁ ^ n :=
by
obtain ⟨b, hbx, hby, hb⟩ := exists_pos_variant h.d_pos a
obtain ⟨n, hn⟩ := h.eq_pow_of_nonneg hbx hby
rcases hb with (rfl | rfl | rfl | hb)
· exact ⟨n, Or.inl (mod_cast hn)⟩
· exact ⟨-n, Or.inl (by simp [hn])⟩
· exact ⟨n, Or.inr (by simp [hn])⟩
· rw [Set.mem_singleton_iff] at hb
rw [hb]
exact ⟨-n, Or.inr (by simp [hn])⟩
