Theorems · Theorem · general algebraic systems

DFinsupp.sumAddHom_apply

∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ)
  (f : Π₀ (i : ι), β i), (DFinsupp.sumAddHom φ) f = f.sum fun x => ⇑(φ x)

While we didn't need decidable instances to define it, we do to reduce it to a sum

Defined in

Mathlib.Data.DFinsupp.BigOperators

Cited by

16 results in Mathlib

Foundations

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

Assumes

DecidableEqAddZeroClassDecidableAddCommMonoid