Documentation

Mathlib.Algebra.BigOperators.Group.Multiset

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 #

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
Instances For
    theorem Multiset.sum.proof_1 {α : Type u_1} [AddCommMonoid α] :
    LeftCommutative fun (x1 x2 : α) => x1 + x2
    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
    Instances For
      theorem Multiset.sum_eq_foldr {α : Type u_3} [AddCommMonoid α] (s : Multiset α) :
      s.sum = Multiset.foldr (fun (x1 x2 : α) => x1 + x2) 0 s
      theorem Multiset.prod_eq_foldr {α : Type u_3} [CommMonoid α] (s : Multiset α) :
      s.prod = Multiset.foldr (fun (x1 x2 : α) => x1 * x2) 1 s
      theorem Multiset.sum_eq_foldl {α : Type u_3} [AddCommMonoid α] (s : Multiset α) :
      s.sum = Multiset.foldl (fun (x1 x2 : α) => x1 + x2) 0 s
      theorem Multiset.prod_eq_foldl {α : Type u_3} [CommMonoid α] (s : Multiset α) :
      s.prod = Multiset.foldl (fun (x1 x2 : α) => x1 * x2) 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 α] :
      @[simp]
      theorem Multiset.prod_zero {α : Type u_3} [CommMonoid α] :
      @[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
      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' ii' mf 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' ii' mf 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' aa' sa' = 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' aa' sa' = 1) :
      s.prod = a ^ Multiset.count a s
      theorem Multiset.sum_eq_zero {α : Type u_3} [AddCommMonoid α] {s : Multiset α} (h : xs, x = 0) :
      s.sum = 0
      theorem Multiset.prod_eq_one {α : Type u_3} [CommMonoid α] {s : Multiset α} (h : xs, x = 1) :
      s.prod = 1
      theorem Multiset.nsmul_count {α : Type u_3} [AddCommMonoid α] {s : Multiset α} [DecidableEq α] (a : α) :
      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_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_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 {α : 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_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_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' {ι : 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₂_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₂_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₂ {ι : 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
      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_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 cr (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 cr (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_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_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_induction {α : Type u_3} [AddCommMonoid α] (p : αProp) (s : Multiset α) (p_mul : ∀ (a b : α), p ap bp (a + b)) (p_one : p 0) (p_s : as, p a) :
      p s.sum
      theorem Multiset.prod_induction {α : Type u_3} [CommMonoid α] (p : αProp) (s : Multiset α) (p_mul : ∀ (a b : α), p ap bp (a * b)) (p_one : p 1) (p_s : as, p a) :
      p s.prod
      theorem Multiset.sum_induction_nonempty {α : Type u_3} [AddCommMonoid α] {s : Multiset α} (p : αProp) (p_mul : ∀ (a b : α), p ap bp (a + b)) (hs : s ) (p_s : as, p a) :
      p s.sum
      theorem Multiset.prod_induction_nonempty {α : Type u_3} [CommMonoid α] {s : Multiset α} (p : αProp) (p_mul : ∀ (a b : α), p ap bp (a * b)) (hs : s ) (p_s : as, 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 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 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 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 AddHom.map_multiset_ne_zero_sum {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] (f : AddHom α β) (s : Multiset α) (hs : s 0) :
      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 Multiset.dvd_prod {α : Type u_3} [CommMonoid α] {s : Multiset α} {a : α} :
      a sa 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 : aS, g1 a g2 a) :
      (Multiset.map g1 S).prod (Multiset.map g2 S).prod

      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' := }
      Instances For
        @[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