Theorems · Theorem · ring theory

Finsupp.prod_finsetProd_comm

∀ {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {s : Finset β}
  (f : α →₀ M) (h : α → M → β → N), (f.prod fun a m => ∏ b ∈ s, h a m b) = ∏ b ∈ s, f.prod fun a m => h a m b

Defined in

Mathlib.Algebra.BigOperators.Finsupp.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

ZeroCommMonoid