# 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`.

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

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

Equations

- Multiset.prod = Multiset.foldr (fun (x1 x2 : M) => x1 * x2) 1

Instances For

source
def Multiset.sum {M : Type u_3} [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

- Multiset.sum = Multiset.foldr (fun (x1 x2 : M) => x1 + x2) 0

Instances For

source
theorem Multiset.prod_eq_foldr {M : Type u_3} [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_3} [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_3} [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_3} [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_3} [CommMonoid M] (l : List M) :
(↑l).prod = l.prod
source
@[simp]
theorem Multiset.sum_coe {M : Type u_3} [AddCommMonoid M] (l : List M) :
(↑l).sum = l.sum
source
@[simp]
theorem Multiset.prod_toList {M : Type u_3} [CommMonoid M] (s : Multiset M) :
s.toList.prod = s.prod
source
@[simp]
theorem Multiset.sum_toList {M : Type u_3} [AddCommMonoid M] (s : Multiset M) :
s.toList.sum = s.sum
source
@[simp]
theorem Multiset.prod_map_toList {ι : Type u_2} {M : Type u_3} [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_2} {M : Type u_3} [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_3} [CommMonoid M] :
prod 0 = 1
source
@[simp]
theorem Multiset.sum_zero {M : Type u_3} [AddCommMonoid M] :
sum 0 = 0
source
@[simp]
theorem Multiset.prod_cons {M : Type u_3} [CommMonoid M] (a : M) (s : Multiset M) :
(a ::ₘ s).prod = a * s.prod
source
@[simp]
theorem Multiset.sum_cons {M : Type u_3} [AddCommMonoid M] (a : M) (s : Multiset M) :
(a ::ₘ s).sum = a + s.sum
source
@[simp]
theorem Multiset.prod_singleton {M : Type u_3} [CommMonoid M] (a : M) :
{a}.prod = a
source
@[simp]
theorem Multiset.sum_singleton {M : Type u_3} [AddCommMonoid M] (a : M) :
{a}.sum = a
source
theorem Multiset.prod_pair {M : Type u_3} [CommMonoid M] (a b : M) :
{a, b}.prod = a * b
source
theorem Multiset.sum_pair {M : Type u_3} [AddCommMonoid M] (a b : M) :
{a, b}.sum = a + b
source
@[simp]
theorem Multiset.prod_replicate {M : Type u_3} [CommMonoid M] (n : ℕ) (a : M) :
(replicate n a).prod = a ^ n
source
@[simp]
theorem Multiset.sum_replicate {M : Type u_3} [AddCommMonoid M] (n : ℕ) (a : M) :
(replicate n a).sum = n • a
source
theorem Multiset.pow_count {M : Type u_3} [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_3} [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_2} {M : Type u_3} {N : Type u_4} [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_2} {M : Type u_3} {N : Type u_4} [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_2} {M : Type u_3} [CommMonoid M] {m : Multiset ι} :
(map (fun (x : ι) => 1) m).prod = 1
source
theorem Multiset.sum_map_zero {ι : Type u_2} {M : Type u_3} [AddCommMonoid M] {m : Multiset ι} :
(map (fun (x : ι) => 0) m).sum = 0
source
theorem Multiset.prod_induction {M : Type u_3} [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 ∈ s, p a) :
p s.prod
source
theorem Multiset.sum_induction {M : Type u_3} [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 ∈ s, p a) :
p s.sum
source
theorem Multiset.prod_induction_nonempty {M : Type u_3} [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 ∈ s, p a) :
p s.prod
source
theorem Multiset.sum_induction_nonempty {M : Type u_3} [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 ∈ s, p a) :
p s.sum