prod_fintype — Mathlib

English

For a finite index type α, and f: α → M with g: α → M → N and h: ∀ i, g i 0 = 1, we have f.prod g = ∑ over i in α of g i (f i).

Русский

Для конечного множества индексов α и f: α → M выполняется равенство: f.prod g = ∑ i, g i (f i).

LaTeX

$$$ f : α \\to M, \\\\text{g} : α \\to M \\to N, \\\\text{h}: \\forall i, g i 0 = 1 \\\\Rightarrow f.prod g = \\prod i, g i (f i) $$$

Lean4

@[to_additive]
theorem prod_fintype [Fintype α] (f : α →₀ M) (g : α → M → N) (h : ∀ i, g i 0 = 1) : f.prod g = ∏ i, g i (f i) :=
  f.prod_of_support_subset (subset_univ _) g fun x _ => h x

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