Documentation

Mathlib.Data.Multiset.Fold

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

fold #

def Multiset.fold {α : Type u_1} (op : ααα) [hc : IsCommutative α op] [ha : IsAssociative α op] :
αMultiset αα

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

Equations
Instances For
    theorem Multiset.fold_eq_foldr {α : Type u_1} (op : ααα) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (s : Multiset α) :
    @[simp]
    theorem Multiset.coe_fold_r {α : Type u_1} (op : ααα) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (l : List α) :
    Multiset.fold op b l = List.foldr op b l
    theorem Multiset.coe_fold_l {α : Type u_1} (op : ααα) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (l : List α) :
    Multiset.fold op b l = List.foldl op b l
    theorem Multiset.fold_eq_foldl {α : Type u_1} (op : ααα) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (s : Multiset α) :
    @[simp]
    theorem Multiset.fold_zero {α : Type u_1} (op : ααα) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) :
    Multiset.fold op b 0 = b
    @[simp]
    theorem Multiset.fold_cons_left {α : Type u_1} (op : ααα) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (a : α) (s : Multiset α) :
    Multiset.fold op b (a ::ₘ s) = op a (Multiset.fold op b s)
    theorem Multiset.fold_cons_right {α : Type u_1} (op : ααα) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (a : α) (s : Multiset α) :
    Multiset.fold op b (a ::ₘ s) = op (Multiset.fold op b s) a
    theorem Multiset.fold_cons'_right {α : Type u_1} (op : ααα) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (a : α) (s : Multiset α) :
    Multiset.fold op b (a ::ₘ s) = Multiset.fold op (op b a) s
    theorem Multiset.fold_cons'_left {α : Type u_1} (op : ααα) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (a : α) (s : Multiset α) :
    Multiset.fold op b (a ::ₘ s) = Multiset.fold op (op a b) s
    theorem Multiset.fold_add {α : Type u_1} (op : ααα) [hc : IsCommutative α op] [ha : IsAssociative α op] (b₁ : α) (b₂ : α) (s₁ : Multiset α) (s₂ : Multiset α) :
    Multiset.fold op (op b₁ b₂) (s₁ + s₂) = op (Multiset.fold op b₁ s₁) (Multiset.fold op b₂ s₂)
    theorem Multiset.fold_bind {α : Type u_1} (op : ααα) [hc : IsCommutative α op] [ha : IsAssociative α op] {ι : Type u_3} (s : Multiset ι) (t : ιMultiset α) (b : ια) (b₀ : α) :
    Multiset.fold op (Multiset.fold op b₀ (Multiset.map b s)) (Multiset.bind s t) = Multiset.fold op b₀ (Multiset.map (fun i => Multiset.fold op (b i) (t i)) s)
    theorem Multiset.fold_singleton {α : Type u_1} (op : ααα) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (a : α) :
    Multiset.fold op b {a} = op a b
    theorem Multiset.fold_distrib {α : Type u_1} {β : Type u_2} (op : ααα) [hc : IsCommutative α op] [ha : IsAssociative α op] {f : βα} {g : βα} (u₁ : α) (u₂ : α) (s : Multiset β) :
    Multiset.fold op (op u₁ u₂) (Multiset.map (fun x => op (f x) (g x)) s) = op (Multiset.fold op u₁ (Multiset.map f s)) (Multiset.fold op u₂ (Multiset.map g s))
    theorem Multiset.fold_hom {α : Type u_1} {β : Type u_2} (op : ααα) [hc : IsCommutative α op] [ha : IsAssociative α op] {op' : βββ} [IsCommutative β op'] [IsAssociative β op'] {m : αβ} (hm : ∀ (x y : α), m (op x y) = op' (m x) (m y)) (b : α) (s : Multiset α) :
    Multiset.fold op' (m b) (Multiset.map m s) = m (Multiset.fold op b s)
    theorem Multiset.fold_union_inter {α : Type u_1} (op : ααα) [hc : IsCommutative α op] [ha : IsAssociative α op] [DecidableEq α] (s₁ : Multiset α) (s₂ : Multiset α) (b₁ : α) (b₂ : α) :
    op (Multiset.fold op b₁ (s₁ s₂)) (Multiset.fold op b₂ (s₁ s₂)) = op (Multiset.fold op b₁ s₁) (Multiset.fold op b₂ s₂)
    @[simp]
    theorem Multiset.fold_dedup_idem {α : Type u_1} (op : ααα) [hc : IsCommutative α op] [ha : IsAssociative α op] [DecidableEq α] [hi : IsIdempotent α op] (s : Multiset α) (b : α) :
    theorem Multiset.max_le_of_forall_le {α : Type u_3} [CanonicallyLinearOrderedAddMonoid α] (l : Multiset α) (n : α) (h : ∀ (x : α), x lx n) :
    theorem Multiset.max_nat_le_of_forall_le (l : Multiset ) (n : ) (h : ∀ (x : ), x lx n) :
    Multiset.fold max 0 l n
    theorem Multiset.le_smul_dedup {α : Type u_1} [DecidableEq α] (s : Multiset α) :
    n, s n Multiset.dedup s