Theorems · Theorem · general algebraic systems

DFinsupp.comp_liftAddHom

∀ {ι : 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.liftAddHom f) = DFinsupp.liftAddHom fun a => g.comp (f a)

The DFinsupp version of Finsupp.comp_liftAddHom

Defined in

Mathlib.Data.DFinsupp.BigOperators

Cited by

4 results in Mathlib

Foundations

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

Assumes

DecidableEqAddZeroClassAddCommMonoidAddCommMonoid