prod_apply — Mathlib

English

Let a be an element and g c be a family of functions indexed by a finite type ι; then

Русский

Пусть a задан и семейство функций g_c индексировано по конечному множеству ι; тогда:

LaTeX

$$$$ \\left( \\prod_{c ∈ \\mathrm{univ}} g_c \\right) a = \\prod_{c ∈ \\mathrm{univ}} g_c(a). $$$$

Lean4

@[to_additive]
theorem prod_apply {α : Type*} {M : α → Type*} [Fintype ι] [∀ a, CommMonoid (M a)] (a : α) (g : ι → ∀ a, M a) :
    (∏ c, g c) a = ∏ c, g c a :=
  Finset.prod_apply a Finset.univ g

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