Theorems · Theorem · general algebraic systems

DFinsupp.sumAddHom_comm

∀ {ι₁ : Type u_4} {ι₂ : Type u_5} {β₁ : ι₁ → Type u_1} {β₂ : ι₂ → Type u_2} {γ : Type u_3} [inst : DecidableEq ι₁]
  [inst_1 : DecidableEq ι₂] [inst_2 : (i : ι₁) → AddZeroClass (β₁ i)] [inst_3 : (i : ι₂) → AddZeroClass (β₂ i)]
  [inst_4 : AddCommMonoid γ] (f₁ : Π₀ (i : ι₁), β₁ i) (f₂ : Π₀ (i : ι₂), β₂ i)
  (h : (i : ι₁) → (j : ι₂) → β₁ i →+ β₂ j →+ γ),
  (DFinsupp.sumAddHom fun i₂ => (DFinsupp.sumAddHom fun i₁ => h i₁ i₂) f₁) f₂ =
    (DFinsupp.sumAddHom fun i₁ => (DFinsupp.sumAddHom fun i₂ => (h i₁ i₂).flip) f₂) f₁

Defined in

Mathlib.Data.DFinsupp.BigOperators

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEqAddZeroClassAddZeroClassAddCommMonoid