prod_eq_prod_coe — Mathlib

English

In a commutative monoid α, for any multiset m, the product of all its elements (counting multiplicities) equals the product m.prod, i.e., m.prod = ∏ x : m, (x : α).

Русский

В коммутативном моноиде α произведение всех элементов мультимножества учётом кратностей равно m.prod, то есть m.prod = ∏ x : m, (x : α).

LaTeX

$$$ m.\mathrm{prod} = \prod x : m, (x : \alpha) $$$

Lean4

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

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