prod_apply — Mathlib

English

For a finite set s and ψ: ι → AddChar(A,M), the action of the product on a is the product of the values: (∏ i∈s ψ(i))(a) = ∏ i∈s ψ(i)(a).

Русский

Для конечного множества s и функции ψ: ι → AddChar(A,M) применение произведения к 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

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

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