Theorems · Theorem · general algebraic systems

DFinsupp.sum_eq_sum_fintype

∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : (i : ι) → Zero (β i)]
  [inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_4 : AddCommMonoid γ] (v : Π₀ (i : ι), β i)
  {f : (i : ι) → β i → γ}, (∀ (i : ι), f i 0 = 0) → v.sum f = ∑ i, f i (DFinsupp.equivFunOnFintype v i)

Defined in

Mathlib.Data.DFinsupp.BigOperators

Cited by

3 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeZeroDecidableAddCommMonoid