Theorems · Definition · general algebraic systems

DFinsupp.sumAddHom

{ι : Type u} →
  {γ : Type w} →
    {β : ι → Type v} →
      [DecidableEq ι] →
        [inst : (i : ι) → AddZeroClass (β i)] →
          [inst_1 : AddCommMonoid γ] → ((i : ι) → β i →+ γ) → (Π₀ (i : ι), β i) →+ γ

When summing over an AddMonoidHom, the decidability assumption is not needed, and the result is also an AddMonoidHom.

Defined in

Mathlib.Data.DFinsupp.BigOperators

Cited by

38 results in Mathlib

Foundations

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

Assumes

DecidableEqAddZeroClassAddCommMonoid