sum_apply_ne_zero_iff_eq_zero — Mathlib

English

For a finite α and additive characters ψ: α → ℂ, the sum ∑_{ψ} ψ(a) is nonzero if and only if a = 0; in particular, ∑_{ψ} ψ(a) ≠ 0 exactly when a = 0.

Русский

Для конечной группы α и аддитивных характеров ψ: α → ℂ сумма ∑_{ψ} ψ(a) не равна нулю тогда и только тогда, когда a = 0.

LaTeX

$$$$ \\sum_{\\psi \ing AddChar(\\alpha, \\mathbb{C})} \\psi(a) \\neq 0 \\quad\\iff\\quad a = 0. $$$$

Lean4

theorem sum_apply_ne_zero_iff_eq_zero [Finite α] : ∑ ψ : AddChar α ℂ, ψ a ≠ 0 ↔ a = 0 :=
  sum_apply_eq_zero_iff_ne_zero.not_left

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