prod_indicator_index — Mathlib

English

Let f : ∀ a ∈ s, M and h : α → M → N with h 0 = 1. Then (indicator s f).prod h equals the attach-product ∏ x ∈ s.attach, h x.1 (f x.1 x.2).

Русский

Пусть f и h заданы так, что h 0 = 1; тогда произведение индикатора по h сводится к произведению по элементам прикрепления.

LaTeX

$$$\big(\operatorname{indicator} s f\big).prod h = \prod_{x \in s.attach} h \ x.1 (f x.1 x.2).$$$

Lean4

@[to_additive]
theorem prod_indicator_index [Zero M] [CommMonoid N] {s : Finset α} (f : α → M) {h : α → M → N}
    (h_zero : ∀ a ∈ s, h a 0 = 1) : (indicator s (fun x _ ↦ f x)).prod h = ∏ x ∈ s, h x (f x) := by
  simp +contextual [h_zero]

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