quadraticChar_sum_zero — Mathlib

English

Over an odd characteristic field, the sum of the quadratic character over all elements is zero.

Русский

В поле с нечетной характеристикой сумма квадратичного знака по всем элементам равна нулю.

LaTeX

$$$\sum_{a\in F} χ_F(a) = 0$$$

Lean4

/-- The sum over the values of the quadratic character is zero when the characteristic is odd. -/
theorem quadraticChar_sum_zero (hF : ringChar F ≠ 2) : ∑ a : F, quadraticChar F a = 0 :=
  sum_eq_zero_of_ne_one (quadraticChar_ne_one hF)

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