prod_toList — Mathlib

English

The product computed from a multiset equals the product computed from its list representation: s.toList.prod = s.prod.

Русский

Произведение, полученное из мультисетa, равно произведению, полученному из его списка: s.toList.prod = s.prod.

LaTeX

$$$s.toList.prod = s.prod$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_toList (s : Multiset M) : s.toList.prod = s.prod :=
  by
  conv_rhs => rw [← coe_toList s]
  rw [prod_coe]

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