Theorems · Theorem · combinatorics

Fintype.sum_sum_type

∀ {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [inst : Fintype α₁] [inst_1 : Fintype α₂] [inst_2 : AddCommMonoid M]
  (f : α₁ ⊕ α₂ → M), ∑ x, f x = ∑ a₁, f (Sum.inl a₁) + ∑ a₂, f (Sum.inr a₂)

Defined in

Mathlib.Data.Fintype.BigOperators

Cited by

22 results in Mathlib

Foundations

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

Assumes

FintypeFintypeAddCommMonoid