prod_multiset_count_of_subset — Mathlib

English

Same as 2351 with a different presentation; the multiset product equals the Finset product over s with counts, given hs.

Русский

Как в 2351, другая формулировка: произведение мультисета равно произведению по Finset с учётом счётчиков.

LaTeX

$$$\displaystyle m.prod = \prod i \in s, i^{m.count i}$, при условии hs$$

Lean4

@[to_additive]
theorem prod_multiset_count_of_subset [DecidableEq M] (m : Multiset M) (s : Finset M) (hs : m.toFinset ⊆ s) :
    m.prod = ∏ i ∈ s, i ^ m.count i := by
  revert hs
  refine Quot.induction_on m fun l => ?_
  simp only [quot_mk_to_coe'', prod_coe, coe_count]
  apply prod_list_count_of_subset l s

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