coe_multiset_prod — Mathlib

English

If all elements of a list lie in a submonoid S, then the list product lies in S.

Русский

Если все элементы списка принадлежат подмоном S, то произведение списка принадлежит S.

LaTeX

$$$\\forall x \\in \\text{l}, x \\in S \\implies \\text{l}.\\operatorname{prod} \\in S$$$

Lean4

@[to_additive (attr := norm_cast, simp)]
theorem coe_multiset_prod {M} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] (m : Multiset S) :
    (m.prod : M) = (m.map (↑)).prod :=
  (SubmonoidClass.subtype S : _ →* M).map_multiset_prod m

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