prod_list_count_of_subset — Mathlib

English

For a list l, the product of its map is equal to the Finset product of elements raised to their counts in the list: prod_list_count.

Русский

Для списка l произведение отображённого списка равно произведению по элементам списка на их счетчики.

LaTeX

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

Lean4

@[to_additive]
theorem prod_list_count_of_subset [DecidableEq M] (m : List M) (s : Finset M) (hs : m.toFinset ⊆ s) :
    m.prod = ∏ i ∈ s, i ^ m.count i := by
  rw [prod_list_count]
  refine prod_subset hs fun x _ hx => ?_
  rw [mem_toFinset] at hx
  rw [count_eq_zero_of_not_mem hx, pow_zero]

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