sum_eq_zero_of_ne_one — Mathlib

English

If χ is nontrivial, the sum over all elements equals zero: ∑ χ(a) = 0.

Русский

Если χ не тривиален, то сумма χ над всеми элементами равна нулю.

LaTeX

$$∑_a χ(a) = 0$$

Lean4

/-- The sum over all values of a nontrivial multiplicative character on a finite ring is zero
(when the target is a domain). -/
theorem sum_eq_zero_of_ne_one [IsDomain R'] {χ : MulChar R R'} (hχ : χ ≠ 1) : ∑ a, χ a = 0 :=
  by
  rcases ne_one_iff.mp hχ with ⟨b, hb⟩
  refine eq_zero_of_mul_eq_self_left hb ?_
  simpa only [Finset.mul_sum, ← map_mul] using b.mulLeft_bijective.sum_comp _

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