Theorems · Theorem · combinatorics

Multiset.prod_map_product_eq_prod_prod

∀ {α : Type u_1} {β : Type v} {M : Type u_4} [inst : CommMonoid M] (s : Multiset α) (t : Multiset β) (f : α × β → M),
  (Multiset.map f (s ×ˢ t)).prod = (Multiset.map (fun i => (Multiset.map (fun j => f (i, j)) t).prod) s).prod

Defined in

Mathlib.Data.Multiset.Bind

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoid