prod_eq_prod_toEnumFinset — Mathlib

English

Let m be a multiset of α. Then the product of the first components over its toEnumFinset equals m.prod, i.e., m.prod = ∏ x ∈ m.toEnumFinset, x.1.

Русский

Пусть m — мультимножество над α. Тогда произведение первых координат по его toEnumFinset равно m.prod, то есть m.prod = ∏ x ∈ m.toEnumFinset, x.1.

LaTeX

$$$ m.\mathrm{prod} = \prod x \in m.\mathrm{toEnumFinset}, x.1 $$$

Lean4

@[to_additive]
theorem prod_eq_prod_toEnumFinset [CommMonoid α] (m : Multiset α) : m.prod = ∏ x ∈ m.toEnumFinset, x.1 :=
  by
  congr
  simp

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