gauss_lemma — Mathlib

English

Let p be prime and a ∈ ℤ with p ∤ a. Then (a/p) = (-1)^{N} where N = #{ x ∈ Ico(1, p/2).succ | p/2 < (a x) mod p}.

Русский

Пусть p — простое число, и a ∈ ℤ так, что p не делится на a. Тогда (a/p) = (-1)^{N}, где N — количество x в Ico(1, p/2).succ, удовлетворяющих p/2 < (a x) mod p.

LaTeX

$$$\left( \frac{a}{p} \right) = (-1)^{\#\{ x \in Ico(1, p/2).succ \mid p/2 < (a \cdot x.cast) \\bmod p \}}$$$

Lean4

/-- **Gauss' lemma**. The Legendre symbol can be computed by considering the number of naturals less
  than `p/2` such that `(a * x) % p > p / 2`. -/
theorem gauss_lemma {p : ℕ} [h : Fact p.Prime] {a : ℤ} (hp : p ≠ 2) (ha0 : (a : ZMod p) ≠ 0) :
    legendreSym p a = (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (a * x.cast : ZMod p).val}) :=
  by
  replace hp : Odd p := h.out.odd_of_ne_two hp
  have :
    (legendreSym p a : ZMod p) =
      (((-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (a * x.cast : ZMod p).val}) : ℤ) : ZMod p) :=
    by rw [legendreSym.eq_pow, gauss_lemma_aux p ha0]
  cases legendreSym.eq_one_or_neg_one p ha0 <;>
      cases neg_one_pow_eq_or ℤ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (a * x.cast : ZMod p).val}) <;>
    simp_all [ne_neg_self hp one_ne_zero, (ne_neg_self hp one_ne_zero).symm]

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