English
Let s be a finite index set and ψ: ι → AddChar(A,M). Then the additive character obtained by summing ψ(i) over i ∈ s, evaluated at a, equals the product of the evaluations: (∑ i∈s ψ(i))(a) = ∏ i∈s ψ(i)(a).
Русский
Пусть s — конечное индексное множество, и ψ: ι → AddChar(A,M). Тогда характер, полученный суммированием ψ(i) по i ∈ s, при аргументе a равен произведению значений: (∑ i∈s ψ(i))(a) = ∏ i∈s ψ(i)(a).
LaTeX
$$$\forall s: \mathrm{Finset}(\iota),\ \forall ψ: \iota \to \mathrm{AddChar}(A,M),\ (\sum_{i\in s} ψ(i))\,a = \prod_{i\in s} (ψ(i)\,a).$$$
Lean4
@[simp, norm_cast]
theorem coe_sum (s : Finset ι) (ψ : ι → AddChar A M) : ∑ i ∈ s, ψ i = ∏ i ∈ s, ⇑(ψ i) := by
induction s using Finset.cons_induction <;> simp [*]
