mathlib documentation

data.multiset.fold

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

fold

def multiset.fold {α : Type u_1} (op : α → α → α) [hc : is_commutative α op] [ha : is_associative α op] :
α → multiset α → α

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

Equations
theorem multiset.fold_eq_foldr {α : Type u_1} (op : α → α → α) [hc : is_commutative α op] [ha : is_associative α op] (b : α) (s : multiset α) :

@[simp]
theorem multiset.coe_fold_r {α : Type u_1} (op : α → α → α) [hc : is_commutative α op] [ha : is_associative α op] (b : α) (l : list α) :

theorem multiset.coe_fold_l {α : Type u_1} (op : α → α → α) [hc : is_commutative α op] [ha : is_associative α op] (b : α) (l : list α) :

theorem multiset.fold_eq_foldl {α : Type u_1} (op : α → α → α) [hc : is_commutative α op] [ha : is_associative α op] (b : α) (s : multiset α) :

@[simp]
theorem multiset.fold_zero {α : Type u_1} (op : α → α → α) [hc : is_commutative α op] [ha : is_associative α op] (b : α) :
multiset.fold op b 0 = b

@[simp]
theorem multiset.fold_cons_left {α : Type u_1} (op : α → α → α) [hc : is_commutative α op] [ha : is_associative α 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 : is_commutative α op] [ha : is_associative α 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 : is_commutative α op] [ha : is_associative α 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 : is_commutative α op] [ha : is_associative α 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 : is_commutative α op] [ha : is_associative α op] (b₁ b₂ : α) (s₁ s₂ : multiset α) :
multiset.fold op (op b₁ b₂) (s₁ + s₂) = op (multiset.fold op b₁ s₁) (multiset.fold op b₂ s₂)

theorem multiset.fold_singleton {α : Type u_1} (op : α → α → α) [hc : is_commutative α op] [ha : is_associative α op] (b a : α) :
multiset.fold op b (a ::ₘ 0) = op a b

theorem multiset.fold_distrib {α : Type u_1} {β : Type u_2} (op : α → α → α) [hc : is_commutative α op] [ha : is_associative α op] {f g : β → α} (u₁ u₂ : α) (s : multiset β) :
multiset.fold op (op u₁ u₂) (multiset.map (λ (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 : is_commutative α op] [ha : is_associative α op] {op' : β → β → β} [is_commutative β op'] [is_associative β 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 : is_commutative α op] [ha : is_associative α op] [decidable_eq α] (s₁ 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_erase_dup_idem {α : Type u_1} (op : α → α → α) [hc : is_commutative α op] [ha : is_associative α op] [decidable_eq α] [hi : is_idempotent α op] (s : multiset α) (b : α) :

theorem multiset.le_smul_erase_dup {α : Type u_1} [decidable_eq α] (s : multiset α) :
∃ (n : ), s n •ℕ s.erase_dup