multiset_prod_singleton — Mathlib

English

The product of singleton images equals the singleton of the product.

Русский

Произведение изображений одиночных множеств равно одиночному множеству произведения.

LaTeX

$$Multiset.map (fun i => { i } ).prod = { Multiset.prod t }$$

Lean4

@[to_additive]
theorem multiset_prod_singleton {M : Type*} [CommMonoid M] (s : Multiset M) :
    (s.map fun i ↦ ({ i } : Set M)).prod = { s.prod } :=
  (map_multiset_prod (singletonMonoidHom : M →* Set M) _).symm

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