Theorems · Theorem · group theory

Finset.prod_mulIndicator_eq_prod_filter

∀ {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [inst : CommMonoid β] (s : Finset ι) (f : ι → κ → β) (t : ι → Set κ)
  (g : ι → κ) [inst_1 : DecidablePred fun i => g i ∈ t i],
  ∏ i ∈ s, (t i).mulIndicator (f i) (g i) = ∏ i ∈ s with g i ∈ t i, f i (g i)

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Indicator

Cited by

4 results in Mathlib

Foundations

Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidDecidablePred