prod_multiset_map_count — Mathlib

English

Let s be a Multiset and f : ι → M. Then the product of the mapped multiset equals the Finset product over s.toFinset with exponent equal to counts: (s.map f).prod = ∏ m ∈ s.toFinset, f m ^ s.count m.

Русский

Пусть s — мультимножество и f — функция; тогда произведение отображённого мультимножества равно произведению по s.toFinset с показателем степени счётов.

LaTeX

$$$\displaystyle (s.map f).prod = \prod m \in s.toFinset, f(m)^{\mathrm{count}(m,s)}$$$

Lean4

@[to_additive]
theorem prod_multiset_map_count [DecidableEq ι] (s : Multiset ι) {M : Type*} [CommMonoid M] (f : ι → M) :
    (s.map f).prod = ∏ m ∈ s.toFinset, f m ^ s.count m :=
  by
  refine Quot.induction_on s fun l => ?_
  simp [prod_list_map_count l f]

Похожие утверждения