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.

@[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_erase {α : Type u_3} [AddCommMonoid α] {s : Multiset α} {a : α} [DecidableEq α] (h : a ∈ s) : a + (s.erase a).sum = s.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_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_add {α : Type u_3} [CommMonoid α] (s t : Multiset α) : (s + t).prod = s.prod * t.prod

@[simp]

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

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

theorem Multiset.sum_nsmul {α : Type u_3} [AddCommMonoid α] (m : Multiset α) (n : ℕ) : (n • m).sum = n • m.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

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_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_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_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_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_one {α : Type u_3} [CommMonoid α] {s : Multiset α} (h : ∀ x ∈ s, x = 1) : s.prod = 1

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

theorem Multiset.prod_hom_ne_zero {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] {s : Multiset α} (hs : s ≠ 0) {F : Type u_7} [FunLike F α β] [MulHomClass F α β] (f : F) : (Multiset.map (⇑f) s).prod = f s.prod

theorem Multiset.sum_hom_ne_zero {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] {s : Multiset α} (hs : s ≠ 0) {F : Type u_7} [FunLike F α β] [AddHomClass 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_7} [FunLike F α β] [MonoidHomClass F α β] (f : F) : (Multiset.map (⇑f) s).prod = f s.prod

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

theorem Multiset.prod_hom' {ι : Type u_2} {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] (s : Multiset ι) {F : Type u_7} [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} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset ι) {F : Type u_7} [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₂_ne_zero {ι : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_6} [CommMonoid α] [CommMonoid β] [CommMonoid γ] {s : Multiset ι} (hs : s ≠ 0) (f : α → β → γ) (hf : ∀ (a b : α) (c d : β), f (a * b) (c * d) = f a c * f b d) (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₂_ne_zero {ι : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_6} [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] {s : Multiset ι} (hs : s ≠ 0) (f : α → β → γ) (hf : ∀ (a b : α) (c d : β), f (a + b) (c + d) = f a c + f b d) (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_6} [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₂ {ι : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_6} [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

@[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

@[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

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_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_prod_map {α : Type u_3} {β' : Type u_5} {γ : Type u_6} [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_map_sum_map {α : Type u_3} {β' : Type u_5} {γ : Type u_6} [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_dvd_prod_of_le {α : Type u_3} [CommMonoid α] {s t : Multiset α} (h : s ≤ t) : s.prod ∣ t.prod

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 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_ne_zero_prod {F : Type u_1} {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] [FunLike F α β] [MulHomClass F α β] (f : F) {s : Multiset α} (hs : s ≠ 0) : f s.prod = (Multiset.map (⇑f) s).prod

theorem map_multiset_ne_zero_sum {F : Type u_1} {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] [FunLike F α β] [AddHomClass F α β] (f : F) {s : Multiset α} (hs : s ≠ 0) : 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 AddMonoidHom.map_multiset_sum {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] (f : α →+ β) (s : Multiset α) : f s.sum = (Multiset.map (⇑f) s).sum

theorem MulHom.map_multiset_ne_zero_prod {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] (f : α →ₙ* β) (s : Multiset α) (hs : s ≠ 0) : f s.prod = (Multiset.map (⇑f) s).prod

theorem AddHom.map_multiset_ne_zero_sum {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] (f : α →ₙ+ β) (s : Multiset α) (hs : s ≠ 0) : f s.sum = (Multiset.map (⇑f) s).sum

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

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.fst_sum {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset (α × β)) : s.sum.1 = (Multiset.map Prod.fst 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.snd_sum {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset (α × β)) : s.sum.2 = (Multiset.map Prod.snd s).sum

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.prod_map_inv' {α : Type u_3} [DivisionCommMonoid α] (m : Multiset α) : (Multiset.map Inv.inv m).prod = m.prod⁻¹

theorem Multiset.sum_map_neg' {α : Type u_3} [SubtractionCommMonoid α] (m : Multiset α) : (Multiset.map Neg.neg m).sum = -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_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_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

@[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

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

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

@[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

theorem Multiset.sum_map_tsub {ι : Type u_2} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] (l : Multiset ι) {f g : ι → α} (hfg : ∀ x ∈ l, g x ≤ f x) : (Multiset.map (fun (x : ι) => f x - g x) l).sum = (Multiset.map f l).sum - (Multiset.map g l).sum