English
If p ∤ a, then (legendreSym p a)^2 = 1.
Русский
Если p не делит a, то (legendreSym p a)^2 = 1.
LaTeX
$$$\big(\mathrm{legendreSym}(p,a)\big)^2 = 1\quad\text{если } a \not\equiv 0 \pmod{p}$$$
Lean4
/-- If `legendreSym p a = -1`, then the only solution of `x^2 - a*y^2 = 0` in `ℤ/pℤ`
is the trivial one. -/
theorem eq_zero_mod_of_eq_neg_one {p : ℕ} [Fact p.Prime] {a : ℤ} (h : legendreSym p a = -1) {x y : ZMod p}
(hxy : x ^ 2 - a * y ^ 2 = 0) : x = 0 ∧ y = 0 :=
by
have ha : (a : ZMod p) ≠ 0 := by
intro hf
rw [(eq_zero_iff p a).mpr hf] at h
simp at h
by_contra hf
rcases imp_iff_or_not.mp (not_and'.mp hf) with hx | hy
· rw [eq_one_of_sq_sub_mul_sq_eq_zero' ha hx hxy, CharZero.eq_neg_self_iff] at h
exact one_ne_zero h
· rw [eq_one_of_sq_sub_mul_sq_eq_zero ha hy hxy, CharZero.eq_neg_self_iff] at h
exact one_ne_zero h
