Theorems · Theorem · general algebraic systems

DFinsupp.sumZeroHom_piSingle

∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : AddCommMonoid γ] (i : ι) (φ : ZeroHom (β i) γ),
  DFinsupp.sumZeroHom (Pi.single i φ) = φ.comp { toFun := fun x => x i, map_zero' := ⋯ }

Defined in

Mathlib.Data.DFinsupp.BigOperators

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqZeroAddCommMonoid