Theorems · Theorem · general algebraic systems

DFinsupp.sum_sub_index

∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddGroup (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommGroup γ] {f g : Π₀ (i : ι), β i}
  {h : (i : ι) → β i → γ},
  (∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂) → (f - g).sum h = f.sum h - g.sum h

Defined in

Mathlib.Data.DFinsupp.BigOperators

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqAddGroupDecidableAddCommGroup