sum_apply — Mathlib

English

Let s be a finite set and ψ: ι → AddChar(A,M). Then (∑ i∈s ψ(i))(a) = ∏ i∈s ψ(i)(a).

Русский

Пусть s — конечный набор и ψ: ι → AddChar(A,M). Тогда (∑ 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

theorem sum_apply (s : Finset ι) (ψ : ι → AddChar A M) (a : A) : (∑ i ∈ s, ψ i) a = ∏ i ∈ s, ψ i a := by
  rw [coe_sum, Finset.prod_apply]

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