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 #

source
def Multiset.prod {M : Type u_2} [CommMonoid M] :
Multiset M → M

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

Equations
Instances For
    source
    def Multiset.sum {M : Type u_2} [AddCommMonoid M] :
    Multiset M → M

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

    Equations
    Instances For
      source
      theorem Multiset.prod_eq_foldr {M : Type u_2} [CommMonoid M] (s : Multiset M) :
      s.prod = foldr (fun (x1 x2 : M) => x1 * x2) 1 s
      source
      theorem Multiset.sum_eq_foldr {M : Type u_2} [AddCommMonoid M] (s : Multiset M) :
      s.sum = foldr (fun (x1 x2 : M) => x1 + x2) 0 s
      source
      theorem Multiset.prod_eq_foldl {M : Type u_2} [CommMonoid M] (s : Multiset M) :
      s.prod = foldl (fun (x1 x2 : M) => x1 * x2) 1 s
      source
      theorem Multiset.sum_eq_foldl {M : Type u_2} [AddCommMonoid M] (s : Multiset M) :
      s.sum = foldl (fun (x1 x2 : M) => x1 + x2) 0 s
      source
      @[simp]
      theorem Multiset.prod_coe {M : Type u_2} [CommMonoid M] (l : List M) :
      (↑l).prod = l.prod
      source
      @[simp]
      theorem Multiset.sum_coe {M : Type u_2} [AddCommMonoid M] (l : List M) :
      (↑l).sum = l.sum
      source
      @[simp]
      theorem Multiset.prod_toList {M : Type u_2} [CommMonoid M] (s : Multiset M) :
      s.toList.prod = s.prod
      source
      @[simp]
      theorem Multiset.sum_toList {M : Type u_2} [AddCommMonoid M] (s : Multiset M) :
      s.toList.sum = s.sum
      source
      @[simp]
      theorem Multiset.prod_map_toList {ι : Type u_1} {M : Type u_2} [CommMonoid M] (s : Multiset ι) (f : ι → M) :
      (List.map f s.toList).prod = (map f s).prod
      source
      @[simp]
      theorem Multiset.sum_map_toList {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (s : Multiset ι) (f : ι → M) :
      (List.map f s.toList).sum = (map f s).sum
      source
      @[simp]
      theorem Multiset.prod_zero {M : Type u_2} [CommMonoid M] :
      prod 0 = 1
      source
      @[simp]
      theorem Multiset.sum_zero {M : Type u_2} [AddCommMonoid M] :
      sum 0 = 0
      source
      @[simp]
      theorem Multiset.prod_cons {M : Type u_2} [CommMonoid M] (a : M) (s : Multiset M) :
      (a ::ₘ s).prod = a * s.prod
      source
      @[simp]
      theorem Multiset.sum_cons {M : Type u_2} [AddCommMonoid M] (a : M) (s : Multiset M) :
      (a ::ₘ s).sum = a + s.sum
      source
      @[simp]
      theorem Multiset.prod_singleton {M : Type u_2} [CommMonoid M] (a : M) :
      {a}.prod = a
      source
      @[simp]
      theorem Multiset.sum_singleton {M : Type u_2} [AddCommMonoid M] (a : M) :
      {a}.sum = a
      source
      theorem Multiset.prod_pair {M : Type u_2} [CommMonoid M] (a b : M) :
      {a, b}.prod = a * b
      source
      theorem Multiset.sum_pair {M : Type u_2} [AddCommMonoid M] (a b : M) :
      {a, b}.sum = a + b
      source
      @[simp]
      theorem Multiset.prod_replicate {M : Type u_2} [CommMonoid M] (n : ℕ) (a : M) :
      (replicate n a).prod = a ^ n
      source
      @[simp]
      theorem Multiset.sum_replicate {M : Type u_2} [AddCommMonoid M] (n : ℕ) (a : M) :
      (replicate n a).sum = n • a
      source
      theorem Multiset.pow_count {M : Type u_2} [CommMonoid M] {s : Multiset M} [DecidableEq M] (a : M) :
      a ^ count a s = (filter (Eq a) s).prod
      source
      theorem Multiset.nsmul_count {M : Type u_2} [AddCommMonoid M] {s : Multiset M} [DecidableEq M] (a : M) :
      count a s • a = (filter (Eq a) s).sum
      source
      theorem Multiset.prod_hom_rel {ι : Type u_1} {M : Type u_2} {N : Type u_3} [CommMonoid M] [CommMonoid N] (s : Multiset ι) {r : M → N → Prop} {f : ι → M} {g : ι → N} (h₁ : r 1 1) (h₂ : ∀ ⦃a : ι⦄ ⦃b : M⦄ ⦃c : N⦄, r b c → r (f a * b) (g a * c)) :
      r (map f s).prod (map g s).prod
      source
      theorem Multiset.sum_hom_rel {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] (s : Multiset ι) {r : M → N → Prop} {f : ι → M} {g : ι → N} (h₁ : r 0 0) (h₂ : ∀ ⦃a : ι⦄ ⦃b : M⦄ ⦃c : N⦄, r b c → r (f a + b) (g a + c)) :
      r (map f s).sum (map g s).sum
      source
      theorem Multiset.prod_map_one {ι : Type u_1} {M : Type u_2} [CommMonoid M] {m : Multiset ι} :
      (map (fun (x : ι) => 1) m).prod = 1
      source
      theorem Multiset.sum_map_zero {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] {m : Multiset ι} :
      (map (fun (x : ι) => 0) m).sum = 0
      source
      theorem Multiset.prod_induction {M : Type u_2} [CommMonoid M] (p : M → Prop) (s : Multiset M) (p_mul : ∀ (a b : M), p a → p b → p (a * b)) (p_one : p 1) (p_s : ∀ (a : M), a ∈ s → p a) :
      p s.prod
      source
      theorem Multiset.sum_induction {M : Type u_2} [AddCommMonoid M] (p : M → Prop) (s : Multiset M) (p_add : ∀ (a b : M), p a → p b → p (a + b)) (p_zero : p 0) (p_s : ∀ (a : M), a ∈ s → p a) :
      p s.sum
      source
      theorem Multiset.prod_induction_nonempty {M : Type u_2} [CommMonoid M] {s : Multiset M} (p : M → Prop) (p_mul : ∀ (a b : M), p a → p b → p (a * b)) (hs : s ≠ ∅) (p_s : ∀ (a : M), a ∈ s → p a) :
      p s.prod
      source
      theorem Multiset.sum_induction_nonempty {M : Type u_2} [AddCommMonoid M] {s : Multiset M} (p : M → Prop) (p_add : ∀ (a b : M), p a → p b → p (a + b)) (hs : s ≠ ∅) (p_s : ∀ (a : M), a ∈ s → p a) :
      p s.sum