instSProd — Mathlib

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

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