Theorems · Theorem · general algebraic systems

DFinsupp.sumAddHom_single

∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i),
  ((DFinsupp.sumAddHom φ) fun₀ | i => x) = (φ i) x

Defined in

Mathlib.Data.DFinsupp.BigOperators

Cited by

17 results in Mathlib

Foundations

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

Assumes

DecidableEqAddZeroClassAddCommMonoid