Theorems · Theorem · general algebraic systems

map_dfinsuppSum

∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {R : Type u_1} {S : Type u_2} {H : Type u_3}
  [inst_1 : (i : ι) → Zero (β i)] [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid R]
  [inst_4 : AddCommMonoid S] [inst_5 : FunLike H R S] [AddMonoidHomClass H R S] (h : H) (f : Π₀ (i : ι), β i)
  (g : (i : ι) → β i → R), h (f.sum g) = f.sum fun a b => h (g a b)

Defined in

Mathlib.Data.DFinsupp.BigOperators

Cited by

7 results in Mathlib

Foundations

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

Assumes

DecidableEqZeroDecidableAddCommMonoidAddCommMonoidFunLikeAddMonoidHomClass