prod_val — Mathlib

English

For any Finset s of elements of M, the product over the underlying multiset equals the finite-set product: s.1.prod = s.prod id.

Русский

Для любого Finset s над элементами M произведение над базовым мультимножеством равно произведению по самому множеству: s.1.prod = s.prod id.

LaTeX

$$$$ s.1.prod = \\; \\prod a \\in s, a. $$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_val [CommMonoid M] (s : Finset M) : s.1.prod = s.prod id := by rw [Finset.prod, Multiset.map_id]

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