Theorems · Theorem · general algebraic systems

DFinsupp.comp_sumAddHom

∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] {δ : Type u_1}
  [inst_1 : (i : ι) → AddZeroClass (β i)] [inst_2 : AddCommMonoid γ] [inst_3 : AddCommMonoid δ] (g : γ →+ δ)
  (f : (i : ι) → β i →+ γ), g.comp (DFinsupp.sumAddHom f) = DFinsupp.sumAddHom fun a => g.comp (f a)

Defined in

Mathlib.Data.DFinsupp.BigOperators

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqAddZeroClassAddCommMonoidAddCommMonoid