sum_apply_eq_zero_iff_ne_zero — Mathlib

English

Let α be a finite group with additive characters ψ: α → ℂ. The sum ∑_{ψ} ψ(a) equals 0 for every a ≠ 0, and equals |α| when a = 0. Equivalently, ∑_{ψ} ψ(a) = 0 if a ≠ 0.

Русский

Пусть α — конечная группа, сопоставляющая каждому элементу a ∈ α сумму по всем характерам ψ: α → ℂ. Эта сумма равна 0 для любого a ≠ 0 и равна |α| при a = 0.

LaTeX

$$$$ \\sum_{\\psi \\in \\mathrm{AddChar}(\\alpha, \\mathbb{C})} \\psi(a) = 0 \\quad \\text{for all } a \\neq 0, \\quad \\text{and } \\sum_{\\psi} \\psi(0) = |\\alpha|.$$$$

Lean4

theorem sum_apply_eq_zero_iff_ne_zero [Finite α] : ∑ ψ : AddChar α ℂ, ψ a = 0 ↔ a ≠ 0 := by
  classical
  cases nonempty_fintype α
  rw [sum_apply_eq_ite, Ne.ite_eq_right_iff]
  exact Nat.cast_ne_zero.2 Fintype.card_ne_zero

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