product_zero — Mathlib

English

The product of a singleton a with a singleton b is the singleton of the pair: ({a} ×ˢ {b}) = {(a,b)}.

Русский

Произведение одиночного элемента a и одиночного элемента b даёт одиночный элемент пары: ({a} ×ˢ {b}) = {(a,b)}.

LaTeX

$$$({ a } : \mathrm{Multiset}\ \alpha) \times^{\mathrm{SProd}} ({ b } : \mathrm{Multiset}\ \beta) = \{(a,b)\}$$$

Lean4

@[simp]
theorem product_zero : s ×ˢ (0 : Multiset β) = 0 := by simp [SProd.sprod, product]

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