Documentation

Mathlib.Algebra.BigOperators.Group.Multiset.Defs

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.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
      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.prod_eq_foldr {α : Type u_3} [CommMonoid α] (s : Multiset α) :
          s.prod = foldr (fun (x1 x2 : α) => x1 * x2) 1 s
          theorem Multiset.sum_eq_foldr {α : Type u_3} [AddCommMonoid α] (s : Multiset α) :
          s.sum = foldr (fun (x1 x2 : α) => x1 + x2) 0 s
          theorem Multiset.prod_eq_foldl {α : Type u_3} [CommMonoid α] (s : Multiset α) :
          s.prod = foldl (fun (x1 x2 : α) => x1 * x2) 1 s
          theorem Multiset.sum_eq_foldl {α : Type u_3} [AddCommMonoid α] (s : Multiset α) :
          s.sum = foldl (fun (x1 x2 : α) => x1 + x2) 0 s
          @[simp]
          theorem Multiset.prod_coe {α : Type u_3} [CommMonoid α] (l : List α) :
          (↑l).prod = l.prod
          @[simp]
          theorem Multiset.sum_coe {α : Type u_3} [AddCommMonoid α] (l : List α) :
          (↑l).sum = l.sum
          @[simp]
          theorem Multiset.prod_toList {α : Type u_3} [CommMonoid α] (s : Multiset α) :
          @[simp]
          theorem Multiset.sum_toList {α : Type u_3} [AddCommMonoid α] (s : Multiset α) :
          @[simp]
          theorem Multiset.prod_zero {α : Type u_3} [CommMonoid α] :
          prod 0 = 1
          @[simp]
          theorem Multiset.sum_zero {α : Type u_3} [AddCommMonoid α] :
          sum 0 = 0
          @[simp]
          theorem Multiset.prod_cons {α : Type u_3} [CommMonoid α] (a : α) (s : Multiset α) :
          (a ::ₘ s).prod = a * s.prod
          @[simp]
          theorem Multiset.sum_cons {α : Type u_3} [AddCommMonoid α] (a : α) (s : Multiset α) :
          (a ::ₘ s).sum = a + s.sum
          @[simp]
          theorem Multiset.prod_singleton {α : Type u_3} [CommMonoid α] (a : α) :
          {a}.prod = a
          @[simp]
          theorem Multiset.sum_singleton {α : Type u_3} [AddCommMonoid α] (a : α) :
          {a}.sum = a
          theorem Multiset.prod_pair {α : Type u_3} [CommMonoid α] (a b : α) :
          {a, b}.prod = a * b
          theorem Multiset.sum_pair {α : Type u_3} [AddCommMonoid α] (a b : α) :
          {a, b}.sum = a + b
          @[simp]
          theorem Multiset.prod_replicate {α : Type u_3} [CommMonoid α] (n : ) (a : α) :
          (replicate n a).prod = a ^ n
          @[simp]
          theorem Multiset.sum_replicate {α : Type u_3} [AddCommMonoid α] (n : ) (a : α) :
          (replicate n a).sum = n a
          theorem Multiset.pow_count {α : Type u_3} [CommMonoid α] {s : Multiset α} [DecidableEq α] (a : α) :
          a ^ count a s = (filter (Eq a) s).prod
          theorem Multiset.nsmul_count {α : Type u_3} [AddCommMonoid α] {s : Multiset α} [DecidableEq α] (a : α) :
          count a s a = (filter (Eq a) 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 (map f s).prod (map g 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 (map f s).sum (map g s).sum
          theorem Multiset.prod_map_one {ι : Type u_2} {α : Type u_3} [CommMonoid α] {m : Multiset ι} :
          (map (fun (x : ι) => 1) m).prod = 1
          theorem Multiset.sum_map_zero {ι : Type u_2} {α : Type u_3} [AddCommMonoid α] {m : Multiset ι} :
          (map (fun (x : ι) => 0) m).sum = 0
          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 {α : 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_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.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