Theorems · Theorem · general algebraic systems

Finsupp.prod_sumElim

∀ {ι₁ : Type u_12} {ι₂ : Type u_13} {α : Type u_14} {M : Type u_15} [inst : Zero α] [inst_1 : CommMonoid M]
  (f₁ : ι₁ →₀ α) (f₂ : ι₂ →₀ α) (g : ι₁ ⊕ ι₂ → α → M),
  (f₁.sumElim f₂).prod g = f₁.prod (g ∘ Sum.inl) * f₂.prod (g ∘ Sum.inr)

Defined in

Mathlib.Data.Finsupp.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

ZeroCommMonoid