English
Let ψ: A → R be an additive character with A finite. Then the total sum ∑ a ψ(a) equals card(A) in the zero case and 0 otherwise: ∑ a ψ(a) = if ψ = 0 then card(A) else 0.
Русский
Пусть ψ: A → R — аддитивный характер, A конечен. Тогда сумма по всем a ∈ A равна card(A) в случае нулевого ψ и равна 0 в противном случае: ∑ a ψ(a) = if ψ = 0 then card(A) else 0.
LaTeX
$$$\sum_{a} ψ(a) = \text{if } ψ = 0 \text{ then } |A| \text{ else } 0,$$$
Lean4
theorem sum_eq_ite (ψ : AddChar A R) [Decidable (ψ = 0)] : ∑ a, ψ a = if ψ = 0 then ↑(card A) else 0 :=
by
split_ifs with h
· simp [h]
obtain ⟨x, hx⟩ := ne_one_iff.1 h
refine eq_zero_of_mul_eq_self_left hx ?_
rw [Finset.mul_sum]
exact Fintype.sum_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_eq_mul ..).symm
