English
There is a canonical product operation on multisets making Multiset α and Multiset β into a structured product with the third component being Multiset (α×β); this operation is defined by s ×ˢ t := Multiset.product s t.
Русский
Существует каноническое произведение мультимножеств, образующее структуру произведения между Multiset α и Multiset β через Multiset.product.
LaTeX
$$$s \times^{\mathrm{SProd}} t := \mathrm{Multiset.product}\; s\; t$$
Lean4
instance instSProd : SProd (Multiset α) (Multiset β) (Multiset (α × β)) where sprod := Multiset.product