The fold operation for a commutative associative operation over a multiset.

fold

def Multiset.fold {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] : α → Multiset α → α

fold op b s folds a commutative associative operation op over the multiset s.

theorem Multiset.fold_eq_foldr {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b : α) (s : Multiset α) : fold op b s = foldr op b s

@[simp]

theorem Multiset.coe_fold_r {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b : α) (l : List α) : fold op b ↑l = List.foldr op b l

theorem Multiset.coe_fold_l {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b : α) (l : List α) : fold op b ↑l = List.foldl op b l

theorem Multiset.fold_eq_foldl {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b : α) (s : Multiset α) : fold op b s = foldl op b s

@[simp]

theorem Multiset.fold_zero {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b : α) : fold op b 0 = b

@[simp]

theorem Multiset.fold_cons_left {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b a : α) (s : Multiset α) : fold op b (a ::ₘ s) = op a (fold op b s)

theorem Multiset.fold_cons_right {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b a : α) (s : Multiset α) : fold op b (a ::ₘ s) = op (fold op b s) a

theorem Multiset.fold_cons'_right {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b a : α) (s : Multiset α) : fold op b (a ::ₘ s) = fold op (op b a) s

theorem Multiset.fold_cons'_left {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b a : α) (s : Multiset α) : fold op b (a ::ₘ s) = fold op (op a b) s

theorem Multiset.fold_add {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b₁ b₂ : α) (s₁ s₂ : Multiset α) : fold op (op b₁ b₂) (s₁ + s₂) = op (fold op b₁ s₁) (fold op b₂ s₂)

theorem Multiset.fold_singleton {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b a : α) : fold op b {a} = op a b

theorem Multiset.fold_distrib {α : Type u_1} {β : Type u_2} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] {f g : β → α} (u₁ u₂ : α) (s : Multiset β) : fold op (op u₁ u₂) (map (fun (x : β) => op (f x) (g x)) s) = op (fold op u₁ (map f s)) (fold op u₂ (map g s))

theorem Multiset.fold_hom {α : Type u_1} {β : Type u_2} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] {op' : β → β → β} [Std.Commutative op'] [Std.Associative op'] {m : α → β} (hm : ∀ (x y : α), m (op x y) = op' (m x) (m y)) (b : α) (s : Multiset α) : fold op' (m b) (map m s) = m (fold op b s)

theorem Multiset.fold_union_inter {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] [DecidableEq α] (s₁ s₂ : Multiset α) (b₁ b₂ : α) : op (fold op b₁ (s₁ ∪ s₂)) (fold op b₂ (s₁ ∩ s₂)) = op (fold op b₁ s₁) (fold op b₂ s₂)

@[simp]

theorem Multiset.fold_dedup_idem {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] [DecidableEq α] [hi : Std.IdempotentOp op] (s : Multiset α) (b : α) : fold op b s.dedup = fold op b s