English
Let s be a finite index set and ψ: ι → AddChar(A,M). Then the additive character obtained by multiplying ψ(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),\ (\prod_{i\in s} ψ(i))\,a = \prod_{i\in s} (ψ(i)\,a).$$$
Lean4
@[simp, norm_cast]
theorem coe_prod (s : Finset ι) (ψ : ι → AddChar A M) : ∏ i ∈ s, ψ i = ∏ i ∈ s, ⇑(ψ i) := by
induction s using Finset.cons_induction <;> simp [*]
