prod_list_count — Mathlib

English

Let l be a list of indices and f a function. Then the product of the mapped list equals the Finset product over l.toFinset with each element raised to its count in l: (l.map f).prod = ∏ m ∈ l.toFinset, f m ^ l.count m.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem prod_list_count [DecidableEq M] (s : List M) : s.prod = ∏ m ∈ s.toFinset, m ^ s.count m := by
  simpa using prod_list_map_count s id

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