prod_toList — Mathlib

English

For any Finset s and function f, the product over the toList of s equals the Finset product: (List.map f s.toList).prod = s.prod f.

Русский

Для любого Finset s и функции f произведение по toList пустику равняется произведению по Finset: (List.map f s.toList).prod = s.prod f.

LaTeX

$$$\\bigl(\\mathrm{List.map} f\\, s.toList\\bigr).\\mathrm{prod} = s.\\mathrm{prod} f$$

Lean4

@[to_additive (attr := simp, grind =)]
theorem prod_toList {M : Type*} [CommMonoid M] (s : Finset M) : s.toList.prod = ∏ x ∈ s, x := by
  simpa using s.prod_map_toList id

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