prod_map_toList — Mathlib

English

For a Finset s and a function f, the product over the mapped Finset s.map e equals the product over s of f composed with e: ∏_{x ∈ s.map e} f x = ∏_{x ∈ s} f (e x).

Русский

Для конечного множества s и отображения f произведение по s.map e равно произведению по s от f ∘ e: ∏_{x ∈ s.map e} f x = ∏_{x ∈ s} f (e x).

LaTeX

$$$\\prod x \\in s.map\\,e, f\\,x = \\prod x \\in s, f (e x)$$$

Lean4

@[to_additive (attr := simp, grind =)]
theorem prod_map_toList (s : Finset ι) (f : ι → M) : (s.toList.map f).prod = s.prod f := by
  rw [Finset.prod, ← Multiset.prod_coe, ← Multiset.map_coe, Finset.coe_toList]

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