sum_smul_sum — Mathlib

English

For multisets s of R and t of M, s.sum • t.sum equals the sum over all pairs (r,m) ∈ s×t of r • m.

Русский

Для мультимножества s из R и t из M верно: s.sum • t.sum = ∑_{(r,m)∈s×t} r • m.

LaTeX

$$$$ s.sum \\cdot t.sum = \\sum_{(r,m) \\in s \\times t} r \\cdot m. $$$$

Lean4

theorem sum_smul_sum {s : Multiset R} {t : Multiset M} :
    s.sum • t.sum = ((s ×ˢ t).map fun p : R × M ↦ p.fst • p.snd).sum := by
  induction s using Multiset.induction with
  | empty => simp
  | cons a s ih => simp [add_smul, ih, ← Multiset.smul_sum]

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