English
For op commutative and associative, the fold distributes over addition of multisets: (s1 + s2).fold op (op b1 b2) = s1.fold op b1 · s2.fold op b2.
Русский
Для коммутативной и ассоциативной операции свёртка распределяется по сложению мультимножества: (s1 + s2).fold op (op b1 b2) = s1.fold op b1 · s2.fold op b2.
LaTeX
$$$ \mathrm{fold} \ op \ (\mathrm{op} \ b_1 \ b_2) \ (s_1 + s_2) = (\mathrm{fold} \ op \ b_1 \ s_1) \cdot (\mathrm{fold} \ op \ b_2 \ s_2) $$$
Lean4
theorem fold_add (b₁ b₂ : α) (s₁ s₂ : Multiset α) : (s₁ + s₂).fold op (b₁ * b₂) = s₁.fold op b₁ * s₂.fold op b₂ :=
Multiset.induction_on s₂ (by rw [Multiset.add_zero, fold_zero, ← fold_cons'_right, ← fold_cons_right op])
(fun a b h => by rw [fold_cons_left, add_cons, fold_cons_left, h, ← ha.assoc, hc.comm a, ha.assoc])
