product — Mathlib

English

The multiplicity of a pair (a,b) in the product s ×ˢ t is the product of the multiplicities of a in s and b in t.

Русский

Число вхождений пары (a,b) в произведение s ×ˢ t равно произведению чисел вхождений a в s и b в t.

LaTeX

$$$(s \times^{\mathrm{SProd}} t).\mathrm{count}(a,b) = s.\mathrm{count}(a) \cdot t.\mathrm{count}(b)$$$

Lean4

/-- The multiplicity of `(a, b)` in `s ×ˢ t` is
  the product of the multiplicity of `a` in `s` and `b` in `t`. -/
def product (s : Multiset α) (t : Multiset β) : Multiset (α × β) :=
  s.bind fun a => t.map <| Prod.mk a

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