Documentation

Mathlib.Algebra.BigOperators.Group.Multiset.Basic

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 #

@[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 : MProp) [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 : MProp) [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' ii' mf 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' ii' mf 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' aa' sa' = 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' aa' sa' = 0) :
s.sum = count a s a
theorem Multiset.prod_eq_one {M : Type u_5} [CommMonoid M] {s : Multiset M} (h : xs, x = 1) :
s.prod = 1
theorem Multiset.sum_eq_zero {M : Type u_5} [AddCommMonoid M] {s : Multiset M} (h : xs, 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 : MNO) (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 : MNO) (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 : MNO) (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 : MNO) (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) :
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 sa s.prod
theorem Multiset.fst_prod {M : Type u_5} {N : Type u_6} [CommMonoid M] [CommMonoid N] (s : Multiset (M × N)) :
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)) :
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 : MN) (h : aS, g1 a g2 a) :
(map g1 S).prod (map g2 S).prod

Multiset.sum, the sum of the elements of a multiset, promoted to a morphism of AddCommMonoids.

Equations
Instances For
    @[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] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] [ContravariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] [Sub M] [OrderedSub M] (l : Multiset ι) {f g : ιM} (hfg : xl, g x f x) :
    (map (fun (x : ι) => f x - g x) l).sum = (map f l).sum - (map g l).sum