Theorems · Theorem · combinatorics

Multiset.prod_toEnumFinset

∀ {α : Type u_1} [inst : DecidableEq α] {β : Type u_3} [inst_1 : CommMonoid β] (m : Multiset α) (f : α → ℕ → β),
  ∏ x ∈ m.toEnumFinset, f x.1 x.2 = ∏ x, f x.fst ↑x.snd

Defined in

Mathlib.Data.Multiset.Fintype

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqCommMonoid