English
For any a ∈ ℤ, the Legendre symbol satisfies legendreSym p a ≡ a^(p/2) (mod p).
Русский
Для любого a ∈ ℤ символ Лежандра удовлетворяет legendreSym p a ≡ a^(p/2) (mod p).
LaTeX
$$$\big(\mathrm{legendreSym}(p,a) : \mathbb{Z}/p\mathbb{Z}\big) = (a : \mathbb{Z}/p\mathbb{Z})^{p/2}$$$
Lean4
/-- We have the congruence `legendreSym p a ≡ a ^ (p / 2) mod p`. -/
theorem eq_pow (a : ℤ) : (legendreSym p a : ZMod p) = (a : ZMod p) ^ (p / 2) :=
by
rcases eq_or_ne (ringChar (ZMod p)) 2 with hc | hc
· by_cases ha : (a : ZMod p) = 0
· rw [legendreSym, ha, quadraticChar_zero, zero_pow (Nat.div_pos (@Fact.out p.Prime).two_le (succ_pos 1)).ne']
norm_cast
· have := (ringChar_zmod_n p).symm.trans hc
subst p
rw [legendreSym, quadraticChar_eq_one_of_char_two hc ha]
revert ha
push_cast
generalize (a : ZMod 2) = b; fin_cases b
· tauto
· simp
· convert quadraticChar_eq_pow_of_char_ne_two' hc (a : ZMod p)
exact (card p).symm
