sum_ne_zero_iff_eq_zero

Mathlib.Algebra.Group.AddChar

URI: https://scilib.ai/kg/mathlib#AddChar.sum_ne_zero_iff_eq_zero

English

Let A be finite, ψ an additive character. Then ∑ x ψ(x) ≠ 0 if and only if ψ = 0.

Русский

Пусть A конечен, ψ — аддитивный характер. Тогда сумма ∑ x ψ(x) не равна нулю тогда и только тогда, когда ψ = 0.

LaTeX

$$$\sum_{x} ψ(x) \neq 0 \quad\iff\quad ψ = 0$$$

Lean4

theorem sum_ne_zero_iff_eq_zero : ∑ x, ψ x ≠ 0 ↔ ψ = 0 :=
  sum_eq_zero_iff_ne_zero.not_left

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru