Theorems · Theorem · group theory

Multiset.mulSupport_fun_pow_count_subset

∀ {α : Type u_1} {M : Type u_2} [inst : DecidableEq α] [inst_1 : CommMonoid M] (s : Multiset α) (f : α → M),
  (Function.mulSupport fun a => f a ^ Multiset.count a s) ⊆ ↑s.toFinset

Defined in

Mathlib.Algebra.BigOperators.Finprod

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqCommMonoid