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 {M : Type u_5} [CommMonoid M] {s : Multiset M} {a : M} [DecidableEq M] (h : a ∈ s) : a * (s.erase a).prod = s.prod

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

theorem Multiset.prod_hom_ne_zero {M : Type u_5} {N : Type u_6} [CommMonoid M] [CommMonoid N] {s : Multiset M} (hs : s ≠ 0) {F : Type u_8} [FunLike F M N] [MulHomClass F M N] (f : F) : (map (⇑f) s).prod = f s.prod

theorem Multiset.sum_hom_ne_zero {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] {s : Multiset M} (hs : s ≠ 0) {F : Type u_8} [FunLike F M N] [AddHomClass F M N] (f : F) : (map (⇑f) s).sum = f s.sum

theorem Multiset.prod_hom {M : Type u_5} {N : Type u_6} [CommMonoid M] [CommMonoid N] (s : Multiset M) {F : Type u_8} [FunLike F M N] [MonoidHomClass F M N] (f : F) : (map (⇑f) s).prod = f s.prod

theorem Multiset.sum_hom {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] (s : Multiset M) {F : Type u_8} [FunLike F M N] [AddMonoidHomClass F M N] (f : F) : (map (⇑f) s).sum = f s.sum

theorem Multiset.prod_hom' {ι : Type u_2} {M : Type u_5} {N : Type u_6} [CommMonoid M] [CommMonoid N] (s : Multiset ι) {F : Type u_8} [FunLike F M N] [MonoidHomClass F M N] (f : F) (g : ι → M) : (map (fun (i : ι) => f (g i)) s).prod = f (map g s).prod

theorem Multiset.sum_hom' {ι : Type u_2} {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] (s : Multiset ι) {F : Type u_8} [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (g : ι → M) : (map (fun (i : ι) => f (g i)) s).sum = f (map g s).sum

theorem Multiset.prod_hom₂_ne_zero {ι : Type u_2} {M : Type u_5} {N : Type u_6} {O : Type u_7} [CommMonoid M] [CommMonoid N] [CommMonoid O] {s : Multiset ι} (hs : s ≠ 0) (f : M → N → O) (hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d) (f₁ : ι → M) (f₂ : ι → N) : (map (fun (i : ι) => f (f₁ i) (f₂ i)) s).prod = f (map f₁ s).prod (map f₂ s).prod

theorem Multiset.sum_hom₂_ne_zero {ι : Type u_2} {M : Type u_5} {N : Type u_6} {O : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid O] {s : Multiset ι} (hs : s ≠ 0) (f : M → N → O) (hf : ∀ (a b : M) (c d : N), f (a + b) (c + d) = f a c + f b d) (f₁ : ι → M) (f₂ : ι → N) : (map (fun (i : ι) => f (f₁ i) (f₂ i)) s).sum = f (map f₁ s).sum (map f₂ s).sum

theorem Multiset.prod_hom₂ {ι : Type u_2} {M : Type u_5} {N : Type u_6} {O : Type u_7} [CommMonoid M] [CommMonoid N] [CommMonoid O] (s : Multiset ι) (f : M → N → O) (hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d) (hf' : f 1 1 = 1) (f₁ : ι → M) (f₂ : ι → N) : (map (fun (i : ι) => f (f₁ i) (f₂ i)) s).prod = f (map f₁ s).prod (map f₂ s).prod

theorem Multiset.sum_hom₂ {ι : Type u_2} {M : Type u_5} {N : Type u_6} {O : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid O] (s : Multiset ι) (f : M → N → O) (hf : ∀ (a b : M) (c d : N), f (a + b) (c + d) = f a c + f b d) (hf' : f 0 0 = 0) (f₁ : ι → M) (f₂ : ι → N) : (map (fun (i : ι) => f (f₁ i) (f₂ i)) s).sum = f (map f₁ s).sum (map f₂ s).sum

@[simp]

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

@[simp]

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

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

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

theorem Multiset.prod_map_prod_map {ι : Type u_2} {κ : Type u_3} {M : Type u_5} [CommMonoid M] (m : Multiset ι) (n : Multiset κ) {f : ι → κ → M} : (map (fun (a : ι) => (map (fun (b : κ) => f a b) n).prod) m).prod = (map (fun (b : κ) => (map (fun (a : ι) => f a b) m).prod) n).prod

theorem Multiset.sum_map_sum_map {ι : Type u_2} {κ : Type u_3} {M : Type u_5} [AddCommMonoid M] (m : Multiset ι) (n : Multiset κ) {f : ι → κ → M} : (map (fun (a : ι) => (map (fun (b : κ) => f a b) n).sum) m).sum = (map (fun (b : κ) => (map (fun (a : ι) => f a b) m).sum) n).sum

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

theorem map_multiset_prod {F : Type u_1} {M : Type u_5} {N : Type u_6} [CommMonoid M] [CommMonoid N] [FunLike F M N] [MonoidHomClass F M N] (f : F) (s : Multiset M) : f s.prod = (Multiset.map (⇑f) s).prod

theorem map_multiset_sum {F : Type u_1} {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (s : Multiset M) : f s.sum = (Multiset.map (⇑f) s).sum

theorem map_multiset_ne_zero_prod {F : Type u_1} {M : Type u_5} {N : Type u_6} [CommMonoid M] [CommMonoid N] [FunLike F M N] [MulHomClass F M N] (f : F) {s : Multiset M} (hs : s ≠ 0) : f s.prod = (Multiset.map (⇑f) s).prod

theorem map_multiset_ne_zero_sum {F : Type u_1} {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [FunLike F M N] [AddHomClass F M N] (f : F) {s : Multiset M} (hs : s ≠ 0) : f s.sum = (Multiset.map (⇑f) s).sum

theorem MonoidHom.map_multiset_prod {M : Type u_5} {N : Type u_6} [CommMonoid M] [CommMonoid N] (f : M →* N) (s : Multiset M) : f s.prod = (Multiset.map (⇑f) s).prod

theorem AddMonoidHom.map_multiset_sum {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] (f : M →+ N) (s : Multiset M) : f s.sum = (Multiset.map (⇑f) s).sum

theorem MulHom.map_multiset_ne_zero_prod {M : Type u_5} {N : Type u_6} [CommMonoid M] [CommMonoid N] (f : M →ₙ* N) (s : Multiset M) (hs : s ≠ 0) : f s.prod = (Multiset.map (⇑f) s).prod

theorem AddHom.map_multiset_ne_zero_sum {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] (f : M →ₙ+ N) (s : Multiset M) (hs : s ≠ 0) : f s.sum = (Multiset.map (⇑f) s).sum

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

theorem Multiset.fst_prod {M : Type u_5} {N : Type u_6} [CommMonoid M] [CommMonoid N] (s : Multiset (M × N)) : s.prod.1 = (map Prod.fst s).prod

theorem Multiset.fst_sum {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] (s : Multiset (M × N)) : s.sum.1 = (map Prod.fst s).sum

theorem Multiset.snd_prod {M : Type u_5} {N : Type u_6} [CommMonoid M] [CommMonoid N] (s : Multiset (M × N)) : s.prod.2 = (map Prod.snd s).prod

theorem Multiset.snd_sum {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] (s : Multiset (M × N)) : s.sum.2 = (map Prod.snd s).sum

theorem Multiset.prod_dvd_prod_of_dvd {M : Type u_5} {N : Type u_6} [CommMonoid N] {S : Multiset M} (g1 g2 : M → N) (h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a) : (map g1 S).prod ∣ (map g2 S).prod

def Multiset.sumAddMonoidHom {M : Type u_5} [AddCommMonoid M] : Multiset M →+ M

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 {M : Type u_5} [AddCommMonoid M] : ⇑sumAddMonoidHom = sum

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

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

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

theorem Multiset.sum_map_tsub {ι : Type u_2} {M : Type u_5} [AddCommMonoid M] [PartialOrder M] [ExistsAddOfLE M] [AddLeftMono M] [AddLeftReflectLE M] [Sub M] [OrderedSub M] (l : Multiset ι) {f g : ι → M} (hfg : ∀ (x : ι), x ∈ l → g x ≤ f x) : (map (fun (x : ι) => f x - g x) l).sum = (map f l).sum - (map g l).sum

instance Multiset.instIsAddTorsionFree {M : Type u_8} : IsAddTorsionFree (Multiset M)