Theorems · Theorem · group theory

finsum_mem_iUnion

∀ {α : Type u_1} {ι : Type u_3} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} [Finite ι] {t : ι → Set α},
  Pairwise (Function.onFun Disjoint t) →
    (∀ (i : ι), (t i).Finite) → ∑ᶠ (a : α) (_ : a ∈ ⋃ i, t i), f a = ∑ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a

Given a family of pairwise disjoint finite sets t i indexed by a finite type, the sum of f a over the union ⋃ i, t i is equal to the sum over all indexes i of the sums of f a over a ∈ t i.

Defined in

Mathlib.Algebra.BigOperators.Finprod

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoidFinite