Documentation

Mathlib.Data.Multiset.Fold

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

fold #

source
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.

Equations
Instances For
    source
    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
    source
    @[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
    source
    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
    source
    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
    source
    @[simp]
    theorem Multiset.fold_zero {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b : α) :
    fold op b 0 = b
    source
    @[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)
    source
    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
    source
    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
    source
    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
    source
    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₂)
    source
    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
    source
    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))
    source
    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)
    source
    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₂)
    source
    @[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