Sums and products over multisets

In this file we define products and sums indexed by multisets. This is later used to define products and sums indexed by finite sets.

Main declarations

• Multiset.prod: s.prod f is the product of f i over all i ∈ s. Not to be mistaken with the cartesian product Multiset.product.
• Multiset.sum: s.sum f is the sum of f i over all i ∈ s.

theorem Multiset.sum.proof_1 {α : Type u_1} [AddCommMonoid α] (x : α) (y : α) (z : α) : x + (y + z) = y + (x + z)

def Multiset.sum {α : Type u_3} [AddCommMonoid α] : Multiset α → α

Sum of a multiset given a commutative additive monoid structure on α. sum {a, b, c} = a + b + c

Equations

• Multiset.sum = Multiset.foldr (fun (x x_1 : α) => x + x_1) ⋯ 0

def Multiset.prod {α : Type u_3} [CommMonoid α] : Multiset α → α

Product of a multiset given a commutative monoid structure on α. prod {a, b, c} = a * b * c

Equations

• Multiset.prod = Multiset.foldr (fun (x x_1 : α) => x * x_1) ⋯ 1

theorem Multiset.sum_eq_foldr {α : Type u_3} [AddCommMonoid α] (s : Multiset α) : s.sum = Multiset.foldr (fun (x x_1 : α) => x + x_1) ⋯ 0 s

theorem Multiset.prod_eq_foldr {α : Type u_3} [CommMonoid α] (s : Multiset α) : s.prod = Multiset.foldr (fun (x x_1 : α) => x * x_1) ⋯ 1 s

theorem Multiset.sum_eq_foldl {α : Type u_3} [AddCommMonoid α] (s : Multiset α) : s.sum = Multiset.foldl (fun (x x_1 : α) => x + x_1) ⋯ 0 s

theorem Multiset.prod_eq_foldl {α : Type u_3} [CommMonoid α] (s : Multiset α) : s.prod = Multiset.foldl (fun (x x_1 : α) => x * x_1) ⋯ 1 s

@[simp]

theorem Multiset.sum_coe {α : Type u_3} [AddCommMonoid α] (l : List α) : (↑l).sum = l.sum

@[simp]

theorem Multiset.prod_coe {α : Type u_3} [CommMonoid α] (l : List α) : (↑l).prod = l.prod

@[simp]

theorem Multiset.sum_toList {α : Type u_3} [AddCommMonoid α] (s : Multiset α) : s.toList.sum = s.sum

@[simp]

theorem Multiset.prod_toList {α : Type u_3} [CommMonoid α] (s : Multiset α) : s.toList.prod = s.prod

@[simp]

theorem Multiset.sum_zero {α : Type u_3} [AddCommMonoid α] : Multiset.sum 0 = 0

@[simp]

theorem Multiset.prod_zero {α : Type u_3} [CommMonoid α] : Multiset.prod 0 = 1

@[simp]

theorem Multiset.sum_cons {α : Type u_3} [AddCommMonoid α] (a : α) (s : Multiset α) : (a ::ₘ s).sum = a + s.sum

@[simp]

theorem Multiset.prod_cons {α : Type u_3} [CommMonoid α] (a : α) (s : Multiset α) : (a ::ₘ s).prod = a * s.prod

@[simp]

theorem Multiset.sum_erase {α : Type u_3} [AddCommMonoid α] {s : Multiset α} {a : α} [DecidableEq α] (h : a ∈ s) : a + (s.erase a).sum = s.sum

@[simp]

theorem Multiset.prod_erase {α : Type u_3} [CommMonoid α] {s : Multiset α} {a : α} [DecidableEq α] (h : a ∈ s) : a * (s.erase a).prod = s.prod

@[simp]

theorem Multiset.sum_map_erase {ι : Type u_2} {α : Type u_3} [AddCommMonoid α] {m : Multiset ι} {f : ι → α} [DecidableEq ι] {a : ι} (h : a ∈ m) : f a + (Multiset.map f (m.erase a)).sum = (Multiset.map f m).sum

@[simp]

theorem Multiset.prod_map_erase {ι : Type u_2} {α : Type u_3} [CommMonoid α] {m : Multiset ι} {f : ι → α} [DecidableEq ι] {a : ι} (h : a ∈ m) : f a * (Multiset.map f (m.erase a)).prod = (Multiset.map f m).prod

@[simp]

theorem Multiset.sum_singleton {α : Type u_3} [AddCommMonoid α] (a : α) : {a}.sum = a

@[simp]

theorem Multiset.prod_singleton {α : Type u_3} [CommMonoid α] (a : α) : {a}.prod = a

theorem Multiset.sum_pair {α : Type u_3} [AddCommMonoid α] (a : α) (b : α) : {a, b}.sum = a + b

theorem Multiset.prod_pair {α : Type u_3} [CommMonoid α] (a : α) (b : α) : {a, b}.prod = a * b

@[simp]

theorem Multiset.sum_add {α : Type u_3} [AddCommMonoid α] (s : Multiset α) (t : Multiset α) : (s + t).sum = s.sum + t.sum

@[simp]

theorem Multiset.prod_add {α : Type u_3} [CommMonoid α] (s : Multiset α) (t : Multiset α) : (s + t).prod = s.prod * t.prod

theorem Multiset.sum_nsmul {α : Type u_3} [AddCommMonoid α] (m : Multiset α) (n : ℕ) : (n • m).sum = n • m.sum

abbrev Multiset.sum_nsmul.match_1 (motive : ℕ → Prop) : ∀ (x : ℕ), (Unit → motive 0) → (∀ (n : ℕ), motive n.succ) → motive x

Equations

• ⋯ = ⋯

theorem Multiset.prod_nsmul {α : Type u_3} [CommMonoid α] (m : Multiset α) (n : ℕ) : (n • m).prod = m.prod ^ n

theorem Multiset.sum_filter_add_sum_filter_not {α : Type u_3} [AddCommMonoid α] {s : Multiset α} (p : α → Prop) [DecidablePred p] : (Multiset.filter p s).sum + (Multiset.filter (fun (a : α) => ¬p a) s).sum = s.sum

theorem Multiset.prod_filter_mul_prod_filter_not {α : Type u_3} [CommMonoid α] {s : Multiset α} (p : α → Prop) [DecidablePred p] : (Multiset.filter p s).prod * (Multiset.filter (fun (a : α) => ¬p a) s).prod = s.prod

@[simp]

theorem Multiset.sum_replicate {α : Type u_3} [AddCommMonoid α] (n : ℕ) (a : α) : (Multiset.replicate n a).sum = n • a

@[simp]

theorem Multiset.prod_replicate {α : Type u_3} [CommMonoid α] (n : ℕ) (a : α) : (Multiset.replicate n a).prod = a ^ n

theorem Multiset.sum_map_eq_nsmul_single {ι : Type u_2} {α : Type u_3} [AddCommMonoid α] {m : Multiset ι} {f : ι → α} [DecidableEq ι] (i : ι) (hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 0) : (Multiset.map f m).sum = Multiset.count i m • f i

theorem Multiset.prod_map_eq_pow_single {ι : Type u_2} {α : Type u_3} [CommMonoid α] {m : Multiset ι} {f : ι → α} [DecidableEq ι] (i : ι) (hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 1) : (Multiset.map f m).prod = f i ^ Multiset.count i m

theorem Multiset.sum_eq_nsmul_single {α : Type u_3} [AddCommMonoid α] {s : Multiset α} [DecidableEq α] (a : α) (h : ∀ (a' : α), a' ≠ a → a' ∈ s → a' = 0) : s.sum = Multiset.count a s • a

theorem Multiset.prod_eq_pow_single {α : Type u_3} [CommMonoid α] {s : Multiset α} [DecidableEq α] (a : α) (h : ∀ (a' : α), a' ≠ a → a' ∈ s → a' = 1) : s.prod = a ^ Multiset.count a s

theorem Multiset.sum_eq_zero {α : Type u_3} [AddCommMonoid α] {s : Multiset α} (h : ∀ x ∈ s, x = 0) : s.sum = 0

theorem Multiset.prod_eq_one {α : Type u_3} [CommMonoid α] {s : Multiset α} (h : ∀ x ∈ s, x = 1) : s.prod = 1

theorem Multiset.nsmul_count {α : Type u_3} [AddCommMonoid α] {s : Multiset α} [DecidableEq α] (a : α) : Multiset.count a s • a = (Multiset.filter (Eq a) s).sum

theorem Multiset.pow_count {α : Type u_3} [CommMonoid α] {s : Multiset α} [DecidableEq α] (a : α) : a ^ Multiset.count a s = (Multiset.filter (Eq a) s).prod

theorem Multiset.sum_hom {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset α) {F : Type u_6} [FunLike F α β] [AddMonoidHomClass F α β] (f : F) : (Multiset.map (⇑f) s).sum = f s.sum

theorem Multiset.prod_hom {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] (s : Multiset α) {F : Type u_6} [FunLike F α β] [MonoidHomClass F α β] (f : F) : (Multiset.map (⇑f) s).prod = f s.prod

theorem Multiset.sum_hom' {ι : Type u_2} {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset ι) {F : Type u_6} [FunLike F α β] [AddMonoidHomClass F α β] (f : F) (g : ι → α) : (Multiset.map (fun (i : ι) => f (g i)) s).sum = f (Multiset.map g s).sum

theorem Multiset.prod_hom' {ι : Type u_2} {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] (s : Multiset ι) {F : Type u_6} [FunLike F α β] [MonoidHomClass F α β] (f : F) (g : ι → α) : (Multiset.map (fun (i : ι) => f (g i)) s).prod = f (Multiset.map g s).prod

theorem Multiset.sum_hom₂ {ι : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] (s : Multiset ι) (f : α → β → γ) (hf : ∀ (a b : α) (c d : β), f (a + b) (c + d) = f a c + f b d) (hf' : f 0 0 = 0) (f₁ : ι → α) (f₂ : ι → β) : (Multiset.map (fun (i : ι) => f (f₁ i) (f₂ i)) s).sum = f (Multiset.map f₁ s).sum (Multiset.map f₂ s).sum

theorem Multiset.prod_hom₂ {ι : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid α] [CommMonoid β] [CommMonoid γ] (s : Multiset ι) (f : α → β → γ) (hf : ∀ (a b : α) (c d : β), f (a * b) (c * d) = f a c * f b d) (hf' : f 1 1 = 1) (f₁ : ι → α) (f₂ : ι → β) : (Multiset.map (fun (i : ι) => f (f₁ i) (f₂ i)) s).prod = f (Multiset.map f₁ s).prod (Multiset.map f₂ s).prod

theorem Multiset.sum_hom_rel {ι : Type u_2} {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset ι) {r : α → β → Prop} {f : ι → α} {g : ι → β} (h₁ : r 0 0) (h₂ : ∀ ⦃a : ι⦄ ⦃b : α⦄ ⦃c : β⦄, r b c → r (f a + b) (g a + c)) : r (Multiset.map f s).sum (Multiset.map g s).sum

theorem Multiset.prod_hom_rel {ι : Type u_2} {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] (s : Multiset ι) {r : α → β → Prop} {f : ι → α} {g : ι → β} (h₁ : r 1 1) (h₂ : ∀ ⦃a : ι⦄ ⦃b : α⦄ ⦃c : β⦄, r b c → r (f a * b) (g a * c)) : r (Multiset.map f s).prod (Multiset.map g s).prod

theorem Multiset.sum_map_zero {ι : Type u_2} {α : Type u_3} [AddCommMonoid α] {m : Multiset ι} : (Multiset.map (fun (x : ι) => 0) m).sum = 0

theorem Multiset.prod_map_one {ι : Type u_2} {α : Type u_3} [CommMonoid α] {m : Multiset ι} : (Multiset.map (fun (x : ι) => 1) m).prod = 1

@[simp]

theorem Multiset.sum_map_add {ι : Type u_2} {α : Type u_3} [AddCommMonoid α] {m : Multiset ι} {f : ι → α} {g : ι → α} : (Multiset.map (fun (i : ι) => f i + g i) m).sum = (Multiset.map f m).sum + (Multiset.map g m).sum

@[simp]

theorem Multiset.prod_map_mul {ι : Type u_2} {α : Type u_3} [CommMonoid α] {m : Multiset ι} {f : ι → α} {g : ι → α} : (Multiset.map (fun (i : ι) => f i * g i) m).prod = (Multiset.map f m).prod * (Multiset.map g m).prod

theorem Multiset.sum_map_nsmul {ι : Type u_2} {α : Type u_3} [AddCommMonoid α] {m : Multiset ι} {f : ι → α} {n : ℕ} : (Multiset.map (fun (i : ι) => n • f i) m).sum = n • (Multiset.map f m).sum

theorem Multiset.prod_map_pow {ι : Type u_2} {α : Type u_3} [CommMonoid α] {m : Multiset ι} {f : ι → α} {n : ℕ} : (Multiset.map (fun (i : ι) => f i ^ n) m).prod = (Multiset.map f m).prod ^ n

theorem Multiset.sum_map_sum_map {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid α] (m : Multiset β) (n : Multiset γ) {f : β → γ → α} : (Multiset.map (fun (a : β) => (Multiset.map (fun (b : γ) => f a b) n).sum) m).sum = (Multiset.map (fun (b : γ) => (Multiset.map (fun (a : β) => f a b) m).sum) n).sum

theorem Multiset.prod_map_prod_map {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid α] (m : Multiset β) (n : Multiset γ) {f : β → γ → α} : (Multiset.map (fun (a : β) => (Multiset.map (fun (b : γ) => f a b) n).prod) m).prod = (Multiset.map (fun (b : γ) => (Multiset.map (fun (a : β) => f a b) m).prod) n).prod

theorem Multiset.sum_induction {α : Type u_3} [AddCommMonoid α] (p : α → Prop) (s : Multiset α) (p_mul : ∀ (a b : α), p a → p b → p (a + b)) (p_one : p 0) (p_s : ∀ a ∈ s, p a) : p s.sum

theorem Multiset.prod_induction {α : Type u_3} [CommMonoid α] (p : α → Prop) (s : Multiset α) (p_mul : ∀ (a b : α), p a → p b → p (a * b)) (p_one : p 1) (p_s : ∀ a ∈ s, p a) : p s.prod

theorem Multiset.sum_induction_nonempty {α : Type u_3} [AddCommMonoid α] {s : Multiset α} (p : α → Prop) (p_mul : ∀ (a b : α), p a → p b → p (a + b)) (hs : s ≠ ∅) (p_s : ∀ a ∈ s, p a) : p s.sum

theorem Multiset.prod_induction_nonempty {α : Type u_3} [CommMonoid α] {s : Multiset α} (p : α → Prop) (p_mul : ∀ (a b : α), p a → p b → p (a * b)) (hs : s ≠ ∅) (p_s : ∀ a ∈ s, p a) : p s.prod

theorem Multiset.prod_dvd_prod_of_le {α : Type u_3} [CommMonoid α] {s : Multiset α} {t : Multiset α} (h : s ≤ t) : s.prod ∣ t.prod

theorem map_multiset_sum {F : Type u_1} {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (f : F) (s : Multiset α) : f s.sum = (Multiset.map (⇑f) s).sum

theorem map_multiset_prod {F : Type u_1} {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] [FunLike F α β] [MonoidHomClass F α β] (f : F) (s : Multiset α) : f s.prod = (Multiset.map (⇑f) s).prod

theorem AddMonoidHom.map_multiset_sum {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] (f : α →+ β) (s : Multiset α) : f s.sum = (Multiset.map (⇑f) s).sum

theorem MonoidHom.map_multiset_prod {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] (f : α →* β) (s : Multiset α) : f s.prod = (Multiset.map (⇑f) s).prod

theorem Multiset.dvd_prod {α : Type u_3} [CommMonoid α] {s : Multiset α} {a : α} : a ∈ s → a ∣ s.prod

theorem Multiset.fst_sum {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset (α × β)) : s.sum.1 = (Multiset.map Prod.fst s).sum

theorem Multiset.fst_prod {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] (s : Multiset (α × β)) : s.prod.1 = (Multiset.map Prod.fst s).prod

theorem Multiset.snd_sum {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset (α × β)) : s.sum.2 = (Multiset.map Prod.snd s).sum

theorem Multiset.snd_prod {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] (s : Multiset (α × β)) : s.prod.2 = (Multiset.map Prod.snd s).prod

theorem Multiset.prod_dvd_prod_of_dvd {α : Type u_3} {β : Type u_4} [CommMonoid β] {S : Multiset α} (g1 : α → β) (g2 : α → β) (h : ∀ a ∈ S, g1 a ∣ g2 a) : (Multiset.map g1 S).prod ∣ (Multiset.map g2 S).prod

def Multiset.sumAddMonoidHom {α : Type u_3} [AddCommMonoid α] : Multiset α →+ α

Multiset.sum, the sum of the elements of a multiset, promoted to a morphism of AddCommMonoids.

Equations

• Multiset.sumAddMonoidHom = { toFun := Multiset.sum, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Multiset.coe_sumAddMonoidHom {α : Type u_3} [AddCommMonoid α] : ⇑Multiset.sumAddMonoidHom = Multiset.sum

theorem Multiset.sum_map_neg' {α : Type u_3} [SubtractionCommMonoid α] (m : Multiset α) : (Multiset.map Neg.neg m).sum = -m.sum

theorem Multiset.prod_map_inv' {α : Type u_3} [DivisionCommMonoid α] (m : Multiset α) : (Multiset.map Inv.inv m).prod = m.prod⁻¹

@[simp]

theorem Multiset.sum_map_neg {ι : Type u_2} {α : Type u_3} [SubtractionCommMonoid α] {m : Multiset ι} {f : ι → α} : (Multiset.map (fun (i : ι) => -f i) m).sum = -(Multiset.map f m).sum

@[simp]

theorem Multiset.prod_map_inv {ι : Type u_2} {α : Type u_3} [DivisionCommMonoid α] {m : Multiset ι} {f : ι → α} : (Multiset.map (fun (i : ι) => (f i)⁻¹) m).prod = (Multiset.map f m).prod⁻¹

@[simp]

theorem Multiset.sum_map_sub {ι : Type u_2} {α : Type u_3} [SubtractionCommMonoid α] {m : Multiset ι} {f : ι → α} {g : ι → α} : (Multiset.map (fun (i : ι) => f i - g i) m).sum = (Multiset.map f m).sum - (Multiset.map g m).sum

@[simp]

theorem Multiset.prod_map_div {ι : Type u_2} {α : Type u_3} [DivisionCommMonoid α] {m : Multiset ι} {f : ι → α} {g : ι → α} : (Multiset.map (fun (i : ι) => f i / g i) m).prod = (Multiset.map f m).prod / (Multiset.map g m).prod

theorem Multiset.sum_map_zsmul {ι : Type u_2} {α : Type u_3} [SubtractionCommMonoid α] {m : Multiset ι} {f : ι → α} {n : ℤ} : (Multiset.map (fun (i : ι) => n • f i) m).sum = n • (Multiset.map f m).sum

theorem Multiset.prod_map_zpow {ι : Type u_2} {α : Type u_3} [DivisionCommMonoid α] {m : Multiset ι} {f : ι → α} {n : ℤ} : (Multiset.map (fun (i : ι) => f i ^ n) m).prod = (Multiset.map f m).prod ^ n

@[simp]

theorem Multiset.sum_map_singleton {α : Type u_3} (s : Multiset α) : (Multiset.map (fun (a : α) => {a}) s).sum = s

theorem Multiset.sum_nat_mod (s : Multiset ℕ) (n : ℕ) : s.sum % n = (Multiset.map (fun (x : ℕ) => x % n) s).sum % n

theorem Multiset.prod_nat_mod (s : Multiset ℕ) (n : ℕ) : s.prod % n = (Multiset.map (fun (x : ℕ) => x % n) s).prod % n

theorem Multiset.sum_int_mod (s : Multiset ℤ) (n : ℤ) : s.sum % n = (Multiset.map (fun (x : ℤ) => x % n) s).sum % n

theorem Multiset.prod_int_mod (s : Multiset ℤ) (n : ℤ) : s.prod % n = (Multiset.map (fun (x : ℤ) => x % n) s).prod % n