Theorems · Theorem · group theory

Finset.sum_indicator_eq_sum_filter

∀ {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [inst : AddCommMonoid β] (s : Finset ι) (f : ι → κ → β) (t : ι → Set κ)
  (g : ι → κ) [inst_1 : DecidablePred fun i => g i ∈ t i],
  ∑ i ∈ s, (t i).indicator (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

5 results in Mathlib

Foundations

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

Assumes

AddCommMonoidDecidablePred