sum_eq_zero_of_ne_one — Mathlib

English

For a finite ring with IsDomain codomain, the sum over all a ∈ R of ψ(a) equals zero if ψ ≠ 1.

Русский

Для конечного кольца и области значений нулевая сумма по всем a ∈ R характеристика ψ(a) тождественно равна нулю, если ψ ≠ 1.

LaTeX

$$∑_{a∈R} ψ(a) = 0$$

Lean4

/-- The sum over the values of a nontrivial additive character vanishes if the target ring
is a domain. -/
theorem sum_eq_zero_of_ne_one [IsDomain R'] {ψ : AddChar R R'} (hψ : ψ ≠ 1) : ∑ a, ψ a = 0 :=
  by
  rcases ne_one_iff.1 hψ with ⟨b, hb⟩
  have h₁ : ∑ a : R, ψ (b + a) = ∑ a : R, ψ a := Fintype.sum_bijective _ (AddGroup.addLeft_bijective b) _ _ fun x => rfl
  simp_rw [map_add_eq_mul] at h₁
  have h₂ : ∑ a : R, ψ a = Finset.univ.sum ↑ψ := rfl
  rw [← Finset.mul_sum, h₂] at h₁
  exact eq_zero_of_mul_eq_self_left hb h₁

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