eq_one_or_neg_one_iff_y_eq_zero — Mathlib

English

For any Pell solution a = (x, y), we have a ∈ {1, -1} if and only if y = 0.

Русский

Для любого решения Пелля a = (x, y) верно: a = 1 или a = −1 тогда и только тогда, когда y = 0.

LaTeX

$$$\forall a\in \mathrm{Solution}_1(d),\; (a = 1 \lor a = -1) \iff a_y = 0$$$

Lean4

/-- A solution is `1` or `-1` if and only if `y = 0`. -/
theorem eq_one_or_neg_one_iff_y_eq_zero {a : Solution₁ d} : a = 1 ∨ a = -1 ↔ a.y = 0 :=
  by
  refine ⟨fun H => H.elim (fun h => by simp [h]) fun h => by simp [h], fun H => ?_⟩
  have prop := a.prop
  rw [H, sq (0 : ℤ), mul_zero, mul_zero, sub_zero, sq_eq_one_iff] at prop
  exact prop.imp (fun h => ext h H) fun h => ext h H

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