add_product — Mathlib

English

The product distributes over addition in the second factor: (s + t) ×ˢ u = s ×ˢ u + t ×ˢ u.

Русский

Произведение распределяется по сумме во втором множителе: (s + t) ×ˢ u = s ×ˢ u + t ×ˢ u.

LaTeX

$$$(s + t) \times^{\mathrm{SProd}} u = s \times^{\mathrm{SProd}} u + t \times^{\mathrm{SProd}} u$$$

Lean4

@[simp]
theorem add_product (s t : Multiset α) (u : Multiset β) : (s + t) ×ˢ u = s ×ˢ u + t ×ˢ u := by
  simp [SProd.sprod, product]

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