prod_multiset_count — Mathlib

English

Given a multiset m, a Finset s, and hs: m.toFinset ⊆ s, the multiset product equals the Finset product with counts: m.prod = ∏ i ∈ s, i ^ m.count i.

Русский

Для мультисета m, множества s и hs: m.toFinset ⊆ s равенство произведений: m.prod = ∏ i ∈ s, i ^ m.count i.

LaTeX

$$$\displaystyle m.prod = \prod i \in s, i^{\mathrm{count}(i,m)}\quad\text{when } m.toFinset \subseteq s$$$

Lean4

@[to_additive]
theorem prod_multiset_count [DecidableEq M] (s : Multiset M) : s.prod = ∏ m ∈ s.toFinset, m ^ s.count m :=
  by
  convert prod_multiset_map_count s id
  rw [Multiset.map_id]

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