English
For lists l1 and l2, the product of their coerced multisets equals the coerced product of the lists: (l1 as Multiset) ×ˢ (l2 as Multiset) = (l1 ×ˢ l2).
Русский
Для списков l1 и l2 произведение их приводимых к множествам множеств равно произведению самих списков в виде множества: (l1 : Multiset α) ×ˢ (l2 : Multiset β) = (l1 ×ˢ l2).
LaTeX
$$$(l_1 : \mathrm{Multiset}\ \alpha) \times^{\mathrm{SProd}} (l_2 : \mathrm{Multiset}\ \beta) = (l_1 \times^{\mathrm{SProd}} l_2)$$$
Lean4
@[simp]
theorem coe_product (l₁ : List α) (l₂ : List β) : (l₁ : Multiset α) ×ˢ (l₂ : Multiset β) = (l₁ ×ˢ l₂) :=
by
dsimp only [SProd.sprod]
rw [product, List.product, ← coe_bind]
simp
