English
The Legendre symbol is multiplicative in a for fixed p: legendreSym p (a b) = legendreSym p a · legendreSym p b.
Русский
Символ Лежандра по переменной a является мультипликативным по фиксированному p: legendreSym p (a b) = legendreSym p a · legendreSym p b.
LaTeX
$$$\mathrm{legendreSym}(p,ab) = \mathrm{legendreSym}(p,a) \cdot \mathrm{legendreSym}(p,b)$$$
Lean4
/-- The Legendre symbol `legendreSym p a = 1` if there is a solution in `ℤ/pℤ`
of the equation `x^2 - a*y^2 = 0` with `y ≠ 0`. -/
theorem eq_one_of_sq_sub_mul_sq_eq_zero {p : ℕ} [Fact p.Prime] {a : ℤ} (ha : (a : ZMod p) ≠ 0) {x y : ZMod p}
(hy : y ≠ 0) (hxy : x ^ 2 - a * y ^ 2 = 0) : legendreSym p a = 1 :=
by
apply_fun (· * y⁻¹ ^ 2) at hxy
simp only [zero_mul] at hxy
rw [(by ring : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = (x * y⁻¹) ^ 2 - a * (y * y⁻¹) ^ 2), mul_inv_cancel₀ hy, one_pow,
mul_one, sub_eq_zero, pow_two] at hxy
exact (eq_one_iff p ha).mpr ⟨x * y⁻¹, hxy.symm⟩
