Theorems · Theorem · combinatorics

Fintype.sum_prod_type

∀ {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [inst : Fintype α₁] [inst_1 : Fintype α₂] [inst_2 : AddCommMonoid γ]
  (f : α₁ × α₂ → γ), ∑ x, f x = ∑ x, ∑ y, f (x, y)

The sum over a product type equals the sum of fiberwise sums. For rewriting in the reverse direction, use Fintype.sum_prod_type'.

Defined in

Mathlib.Data.Fintype.BigOperators

Cited by

6 results in Mathlib

Foundations

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

Assumes

FintypeFintypeAddCommMonoid