English
For an odd prime p and odd a with a not divisible by p, the Legendre symbol (p|a) equals (-1) raised to the sum over x ∈ Ico 1 (p/2).succ of x*a/p.
Русский
Для нечетного простого p и нечетного a, не делящегося на p, символ Лежандра (p|a) равен (-1) в степени суммы по x ∈ Ico 1 (p/2).succ от x*a/p.
LaTeX
$$$\operatorname{legendreSym} p a = (-1)^{\sum_{x ∈ Ico 1 (p / 2).succ} x * a / p}$$$
Lean4
/-- **Eisenstein's lemma** -/
theorem eisenstein_lemma {p : ℕ} [Fact p.Prime] (hp : p ≠ 2) {a : ℕ} (ha1 : a % 2 = 1) (ha0 : (a : ZMod p) ≠ 0) :
legendreSym p a = (-1) ^ ∑ x ∈ Ico 1 (p / 2).succ, x * a / p :=
by
haveI hp' : Fact (p % 2 = 1) := ⟨(Nat.Prime.mod_two_eq_one_iff_ne_two Fact.out).mpr hp⟩
have ha0' : ((a : ℤ) : ZMod p) ≠ 0 := by norm_cast
rw [neg_one_pow_eq_pow_mod_two, gauss_lemma hp ha0', neg_one_pow_eq_pow_mod_two,
(by norm_cast : ((a : ℤ) : ZMod p) = (a : ZMod p)), show _ = _ from eisenstein_lemma_aux p ha1 ha0]
