Documentation

Mathlib.Algebra.BigOperators.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 #

• Multiset.prod: s.prod f is the product of f i over all i ∈ s∈ 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∈ s.

Implementation notes #

Nov 2022: To speed the Lean 4 port, lemmas requiring extra algebra imports (data.list.big_operators.lemmas rather than .basic) have been moved to a separate file, algebra.big_operators.multiset.lemmas. This split does not need to be permanent.

def Multiset.sum.proof_1 {α : Type u_1} [inst : ] (x : α) (y : α) (z : α) :
x + (y + z) = y + (x + z)
Equations
• (_ : x + (y + z) = y + (x + z)) = (_ : x + (y + z) = y + (x + z))
def Multiset.sum {α : Type u_1} [inst : ] :
α

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

Equations
def Multiset.prod {α : Type u_1} [inst : ] :
α

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

Equations
• Multiset.prod = Multiset.foldr (fun x x_1 => x * x_1) (_ : ∀ (x y z : α), x * (y * z) = y * (x * z)) 1
theorem Multiset.sum_eq_foldr {α : Type u_1} [inst : ] (s : ) :
= Multiset.foldr (fun x x_1 => x + x_1) (_ : ∀ (x y z : α), x + (y + z) = y + (x + z)) 0 s
theorem Multiset.prod_eq_foldr {α : Type u_1} [inst : ] (s : ) :
= Multiset.foldr (fun x x_1 => x * x_1) (_ : ∀ (x y z : α), x * (y * z) = y * (x * z)) 1 s
theorem Multiset.sum_eq_foldl {α : Type u_1} [inst : ] (s : ) :
= Multiset.foldl (fun x x_1 => x + x_1) (_ : ∀ (x y z : α), x + y + z = x + z + y) 0 s
theorem Multiset.prod_eq_foldl {α : Type u_1} [inst : ] (s : ) :
= Multiset.foldl (fun x x_1 => x * x_1) (_ : ∀ (x y z : α), x * y * z = x * z * y) 1 s
@[simp]
theorem Multiset.coe_sum {α : Type u_1} [inst : ] (l : List α) :
@[simp]
theorem Multiset.coe_prod {α : Type u_1} [inst : ] (l : List α) :
@[simp]
theorem Multiset.sum_toList {α : Type u_1} [inst : ] (s : ) :
@[simp]
theorem Multiset.prod_toList {α : Type u_1} [inst : ] (s : ) :
@[simp]
theorem Multiset.sum_zero {α : Type u_1} [inst : ] :
@[simp]
theorem Multiset.prod_zero {α : Type u_1} [inst : ] :
@[simp]
theorem Multiset.sum_cons {α : Type u_1} [inst : ] (a : α) (s : ) :
@[simp]
theorem Multiset.prod_cons {α : Type u_1} [inst : ] (a : α) (s : ) :
@[simp]
theorem Multiset.sum_erase {α : Type u_1} [inst : ] {s : } {a : α} [inst : ] (h : a s) :
a + =
@[simp]
theorem Multiset.prod_erase {α : Type u_1} [inst : ] {s : } {a : α} [inst : ] (h : a s) :
a * =
@[simp]
theorem Multiset.sum_map_erase {ι : Type u_1} {α : Type u_2} [inst : ] {m : } {f : ια} [inst : ] {a : ι} (h : a m) :
@[simp]
theorem Multiset.prod_map_erase {ι : Type u_1} {α : Type u_2} [inst : ] {m : } {f : ια} [inst : ] {a : ι} (h : a m) :
@[simp]
theorem Multiset.sum_singleton {α : Type u_1} [inst : ] (a : α) :
@[simp]
theorem Multiset.prod_singleton {α : Type u_1} [inst : ] (a : α) :
= a
theorem Multiset.sum_pair {α : Type u_1} [inst : ] (a : α) (b : α) :
Multiset.sum {a, b} = a + b
theorem Multiset.prod_pair {α : Type u_1} [inst : ] (a : α) (b : α) :
Multiset.prod {a, b} = a * b
@[simp]
theorem Multiset.sum_add {α : Type u_1} [inst : ] (s : ) (t : ) :
@[simp]
theorem Multiset.prod_add {α : Type u_1} [inst : ] (s : ) (t : ) :
theorem Multiset.prod_nsmul {α : Type u_1} [inst : ] (m : ) (n : ) :
@[simp]
theorem Multiset.sum_replicate {α : Type u_1} [inst : ] (n : ) (a : α) :
= n a
@[simp]
theorem Multiset.prod_replicate {α : Type u_1} [inst : ] (n : ) (a : α) :
= a ^ n
theorem Multiset.sum_map_eq_nsmul_single {ι : Type u_1} {α : Type u_2} [inst : ] {m : } {f : ια} [inst : ] (i : ι) (hf : ∀ (i' : ι), i' ii' mf i' = 0) :
theorem Multiset.prod_map_eq_pow_single {ι : Type u_1} {α : Type u_2} [inst : ] {m : } {f : ια} [inst : ] (i : ι) (hf : ∀ (i' : ι), i' ii' mf i' = 1) :
= f i ^
theorem Multiset.sum_eq_nsmul_single {α : Type u_1} [inst : ] {s : } [inst : ] (a : α) (h : ∀ (a' : α), a' aa' sa' = 0) :
= a
theorem Multiset.prod_eq_pow_single {α : Type u_1} [inst : ] {s : } [inst : ] (a : α) (h : ∀ (a' : α), a' aa' sa' = 1) :
= a ^
theorem Multiset.nsmul_count {α : Type u_1} [inst : ] {s : } [inst : ] (a : α) :
theorem Multiset.pow_count {α : Type u_1} [inst : ] {s : } [inst : ] (a : α) :
theorem Multiset.sum_hom {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] (s : ) {F : Type u_3} [inst : ] (f : F) :
Multiset.sum (Multiset.map (f) s) = f ()
theorem Multiset.prod_hom {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] (s : ) {F : Type u_3} [inst : ] (f : F) :
Multiset.prod (Multiset.map (f) s) = f ()
theorem Multiset.sum_hom' {ι : Type u_2} {α : Type u_4} {β : Type u_1} [inst : ] [inst : ] (s : ) {F : Type u_3} [inst : ] (f : F) (g : ια) :
Multiset.sum (Multiset.map (fun i => f (g i)) s) = f (Multiset.sum ())
theorem Multiset.prod_hom' {ι : Type u_2} {α : Type u_4} {β : Type u_1} [inst : ] [inst : ] (s : ) {F : Type u_3} [inst : ] (f : F) (g : ια) :
Multiset.prod (Multiset.map (fun i => f (g i)) s) = f ()
theorem Multiset.sum_hom₂ {ι : Type u_3} {α : Type u_4} {β : Type u_1} {γ : Type u_2} [inst : ] [inst : ] [inst : ] (s : ) (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.sum (Multiset.map (fun i => f (f₁ i) (f₂ i)) s) = f (Multiset.sum (Multiset.map f₁ s)) (Multiset.sum (Multiset.map f₂ s))
theorem Multiset.prod_hom₂ {ι : Type u_3} {α : Type u_4} {β : Type u_1} {γ : Type u_2} [inst : ] [inst : ] [inst : ] (s : ) (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.prod (Multiset.map (fun i => f (f₁ i) (f₂ i)) s) = f (Multiset.prod (Multiset.map f₁ s)) (Multiset.prod (Multiset.map f₂ s))
theorem Multiset.sum_hom_rel {ι : Type u_2} {α : Type u_3} {β : Type u_1} [inst : ] [inst : ] (s : ) {r : αβProp} {f : ια} {g : ιβ} (h₁ : r 0 0) (h₂ : a : ι⦄ → b : α⦄ → c : β⦄ → r b cr (f a + b) (g a + c)) :
theorem Multiset.prod_hom_rel {ι : Type u_2} {α : Type u_3} {β : Type u_1} [inst : ] [inst : ] (s : ) {r : αβProp} {f : ια} {g : ιβ} (h₁ : r 1 1) (h₂ : a : ι⦄ → b : α⦄ → c : β⦄ → r b cr (f a * b) (g a * c)) :
r () ()
theorem Multiset.sum_map_zero {ι : Type u_2} {α : Type u_1} [inst : ] {m : } :
Multiset.sum (Multiset.map (fun x => 0) m) = 0
theorem Multiset.prod_map_one {ι : Type u_2} {α : Type u_1} [inst : ] {m : } :
Multiset.prod (Multiset.map (fun x => 1) m) = 1
@[simp]
theorem Multiset.sum_map_add {ι : Type u_2} {α : Type u_1} [inst : ] {m : } {f : ια} {g : ια} :
Multiset.sum (Multiset.map (fun i => f i + g i) m) = Multiset.sum () + Multiset.sum ()
@[simp]
theorem Multiset.prod_map_mul {ι : Type u_2} {α : Type u_1} [inst : ] {m : } {f : ια} {g : ια} :
Multiset.prod (Multiset.map (fun i => f i * g i) m) = *
@[simp]
theorem Multiset.prod_map_neg {α : Type u_1} [inst : ] [inst : ] (s : ) :
Multiset.prod (Multiset.map Neg.neg s) = (-1) ^ Multiset.card s *
theorem Multiset.sum_map_nsmul {ι : Type u_2} {α : Type u_1} [inst : ] {m : } {f : ια} {n : } :
Multiset.sum (Multiset.map (fun i => n f i) m) = n Multiset.sum ()
theorem Multiset.prod_map_pow {ι : Type u_2} {α : Type u_1} [inst : ] {m : } {f : ια} {n : } :
Multiset.prod (Multiset.map (fun i => f i ^ n) m) = ^ n
theorem Multiset.sum_map_sum_map {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : ] (m : ) (n : ) {f : βγα} :
Multiset.sum (Multiset.map (fun a => Multiset.sum (Multiset.map (fun b => f a b) n)) m) = Multiset.sum (Multiset.map (fun b => Multiset.sum (Multiset.map (fun a => f a b) m)) n)
theorem Multiset.prod_map_prod_map {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : ] (m : ) (n : ) {f : βγα} :
Multiset.prod (Multiset.map (fun a => Multiset.prod (Multiset.map (fun b => f a b) n)) m) = Multiset.prod (Multiset.map (fun b => Multiset.prod (Multiset.map (fun a => f a b) m)) n)
theorem Multiset.sum_induction {α : Type u_1} [inst : ] (p : αProp) (s : ) (p_mul : (a b : α) → p ap bp (a + b)) (p_one : p 0) (p_s : (a : α) → a sp a) :
p ()
theorem Multiset.prod_induction {α : Type u_1} [inst : ] (p : αProp) (s : ) (p_mul : (a b : α) → p ap bp (a * b)) (p_one : p 1) (p_s : (a : α) → a sp a) :
p ()
theorem Multiset.sum_induction_nonempty {α : Type u_1} [inst : ] {s : } (p : αProp) (p_mul : (a b : α) → p ap bp (a + b)) (hs : s ) (p_s : (a : α) → a sp a) :
p ()
theorem Multiset.prod_induction_nonempty {α : Type u_1} [inst : ] {s : } (p : αProp) (p_mul : (a b : α) → p ap bp (a * b)) (hs : s ) (p_s : (a : α) → a sp a) :
p ()
theorem Multiset.prod_dvd_prod_of_le {α : Type u_1} [inst : ] {s : } {t : } (h : s t) :
theorem Multiset.prod_dvd_prod_of_dvd {α : Type u_2} {β : Type u_1} [inst : ] {S : } (g1 : αβ) (g2 : αβ) (h : ∀ (a : α), a Sg1 a g2 a) :
def Multiset.sumAddMonoidHom {α : Type u_1} [inst : ] :
→+ α

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

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Multiset.coe_sumAddMonoidHom {α : Type u_1} [inst : ] :
theorem Multiset.prod_eq_zero {α : Type u_1} [inst : ] {s : } (h : 0 s) :
theorem Multiset.prod_eq_zero_iff {α : Type u_1} [inst : ] [inst : ] [inst : ] {s : } :
0 s
theorem Multiset.prod_ne_zero {α : Type u_1} [inst : ] [inst : ] [inst : ] {s : } (h : ¬0 s) :
theorem Multiset.sum_map_neg' {α : Type u_1} [inst : ] (m : ) :
theorem Multiset.prod_map_inv' {α : Type u_1} [inst : ] (m : ) :
@[simp]
theorem Multiset.sum_map_neg {ι : Type u_2} {α : Type u_1} [inst : ] {m : } {f : ια} :
@[simp]
theorem Multiset.prod_map_inv {ι : Type u_2} {α : Type u_1} [inst : ] {m : } {f : ια} :
Multiset.prod (Multiset.map (fun i => (f i)⁻¹) m) = ()⁻¹
@[simp]
theorem Multiset.sum_map_sub {ι : Type u_2} {α : Type u_1} [inst : ] {m : } {f : ια} {g : ια} :
Multiset.sum (Multiset.map (fun i => f i - g i) m) = Multiset.sum () - Multiset.sum ()
@[simp]
theorem Multiset.prod_map_div {ι : Type u_2} {α : Type u_1} [inst : ] {m : } {f : ια} {g : ια} :
Multiset.prod (Multiset.map (fun i => f i / g i) m) = /
theorem Multiset.sum_map_zsmul {ι : Type u_2} {α : Type u_1} [inst : ] {m : } {f : ια} {n : } :
Multiset.sum (Multiset.map (fun i => n f i) m) = n Multiset.sum ()
theorem Multiset.prod_map_zpow {ι : Type u_2} {α : Type u_1} [inst : ] {m : } {f : ια} {n : } :
Multiset.prod (Multiset.map (fun i => f i ^ n) m) = ^ n
theorem Multiset.sum_map_mul_left {ι : Type u_2} {α : Type u_1} [inst : ] {a : α} {s : } {f : ια} :
Multiset.sum (Multiset.map (fun i => a * f i) s) = a * Multiset.sum ()
theorem Multiset.sum_map_mul_right {ι : Type u_2} {α : Type u_1} [inst : ] {a : α} {s : } {f : ια} :
Multiset.sum (Multiset.map (fun i => f i * a) s) = Multiset.sum () * a
theorem Multiset.dvd_sum {α : Type u_1} [inst : ] {a : α} {s : } :
(∀ (x : α), x sa x) →

Order #

theorem Multiset.sum_nonneg {α : Type u_1} [inst : ] {s : } :
(∀ (x : α), x s0 x) →
theorem Multiset.one_le_prod_of_one_le {α : Type u_1} [inst : ] {s : } :
(∀ (x : α), x s1 x) →
theorem Multiset.single_le_sum {α : Type u_1} [inst : ] {s : } :
(∀ (x : α), x s0 x) → ∀ (x : α), x s
theorem Multiset.single_le_prod {α : Type u_1} [inst : ] {s : } :
(∀ (x : α), x s1 x) → ∀ (x : α), x s
theorem Multiset.sum_le_card_nsmul {α : Type u_1} [inst : ] (s : ) (n : α) (h : ∀ (x : α), x sx n) :
Multiset.card s n
theorem Multiset.prod_le_pow_card {α : Type u_1} [inst : ] (s : ) (n : α) (h : ∀ (x : α), x sx n) :
n ^ Multiset.card s
theorem Multiset.all_zero_of_le_zero_le_of_sum_eq_zero {α : Type u_1} [inst : ] {s : } :
(∀ (x : α), x s0 x) → ∀ (x : α), x sx = 0
theorem Multiset.all_one_of_le_one_le_of_prod_eq_one {α : Type u_1} [inst : ] {s : } :
(∀ (x : α), x s1 x) → ∀ (x : α), x sx = 1
theorem Multiset.sum_le_sum_of_rel_le {α : Type u_1} [inst : ] {s : } {t : } (h : Multiset.Rel (fun x x_1 => x x_1) s t) :
theorem Multiset.prod_le_prod_of_rel_le {α : Type u_1} [inst : ] {s : } {t : } (h : Multiset.Rel (fun x x_1 => x x_1) s t) :
theorem Multiset.sum_map_le_sum_map {ι : Type u_1} {α : Type u_2} [inst : ] {s : } (f : ια) (g : ια) (h : ∀ (i : ι), i sf i g i) :
theorem Multiset.prod_map_le_prod_map {ι : Type u_1} {α : Type u_2} [inst : ] {s : } (f : ια) (g : ια) (h : ∀ (i : ι), i sf i g i) :
theorem Multiset.sum_map_le_sum {α : Type u_1} [inst : ] {s : } (f : αα) (h : ∀ (x : α), x sf x x) :
theorem Multiset.prod_map_le_prod {α : Type u_1} [inst : ] {s : } (f : αα) (h : ∀ (x : α), x sf x x) :
theorem Multiset.sum_le_sum_map {α : Type u_1} [inst : ] {s : } (f : αα) (h : ∀ (x : α), x sx f x) :
theorem Multiset.prod_le_prod_map {α : Type u_1} [inst : ] {s : } (f : αα) (h : ∀ (x : α), x sx f x) :
theorem Multiset.card_nsmul_le_sum {α : Type u_1} [inst : ] {s : } {a : α} (h : ∀ (x : α), x sa x) :
Multiset.card s a
theorem Multiset.pow_card_le_prod {α : Type u_1} [inst : ] {s : } {a : α} (h : ∀ (x : α), x sa x) :
a ^ Multiset.card s
theorem Multiset.prod_nonneg {α : Type u_1} [inst : ] {m : } (h : ∀ (a : α), a m0 a) :
theorem Multiset.sum_eq_zero {α : Type u_1} [inst : ] {m : } (h : ∀ (x : α), x mx = 0) :

Slightly more general version of Multiset.sum_eq_zero_iff for a non-ordered AddMonoid

theorem Multiset.prod_eq_one {α : Type u_1} [inst : ] {m : } (h : ∀ (x : α), x mx = 1) :

Slightly more general version of Multiset.prod_eq_one_iff for a non-ordered Monoid

theorem Multiset.le_sum_of_mem {α : Type u_1} [inst : ] {m : } {a : α} (h : a m) :
theorem Multiset.le_prod_of_mem {α : Type u_1} [inst : ] {m : } {a : α} (h : a m) :
theorem Multiset.le_sum_of_subadditive_on_pred {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : αβ) (p : αProp) (h_one : f 0 = 0) (hp_one : p 0) (h_mul : ∀ (a b : α), p ap bf (a + b) f a + f b) (hp_mul : (a b : α) → p ap bp (a + b)) (s : ) (hps : (a : α) → a sp a) :
theorem Multiset.le_prod_of_submultiplicative_on_pred {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : αβ) (p : αProp) (h_one : f 1 = 1) (hp_one : p 1) (h_mul : ∀ (a b : α), p ap bf (a * b) f a * f b) (hp_mul : (a b : α) → p ap bp (a * b)) (s : ) (hps : (a : α) → a sp a) :
f ()
theorem Multiset.le_sum_of_subadditive {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : αβ) (h_one : f 0 = 0) (h_mul : ∀ (a b : α), f (a + b) f a + f b) (s : ) :
theorem Multiset.le_prod_of_submultiplicative {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : αβ) (h_one : f 1 = 1) (h_mul : ∀ (a b : α), f (a * b) f a * f b) (s : ) :
f ()
theorem Multiset.le_sum_nonempty_of_subadditive_on_pred {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : αβ) (p : αProp) (h_mul : ∀ (a b : α), p ap bf (a + b) f a + f b) (hp_mul : (a b : α) → p ap bp (a + b)) (s : ) (hs_nonempty : s ) (hs : (a : α) → a sp a) :
theorem Multiset.le_prod_nonempty_of_submultiplicative_on_pred {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : αβ) (p : αProp) (h_mul : ∀ (a b : α), p ap bf (a * b) f a * f b) (hp_mul : (a b : α) → p ap bp (a * b)) (s : ) (hs_nonempty : s ) (hs : (a : α) → a sp a) :
f ()
theorem Multiset.le_sum_nonempty_of_subadditive {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : αβ) (h_mul : ∀ (a b : α), f (a + b) f a + f b) (s : ) (hs_nonempty : s ) :
theorem Multiset.le_prod_nonempty_of_submultiplicative {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : αβ) (h_mul : ∀ (a b : α), f (a * b) f a * f b) (s : ) (hs_nonempty : s ) :
f ()
@[simp]
theorem Multiset.sum_map_singleton {α : Type u_1} (s : ) :
Multiset.sum (Multiset.map (fun a => {a}) s) = s
theorem Multiset.abs_sum_le_sum_abs {α : Type u_1} [inst : ] {s : } :
theorem Multiset.sum_nat_mod (s : ) (n : ) :
= Multiset.sum (Multiset.map (fun x => x % n) s) % n
theorem Multiset.prod_nat_mod (s : ) (n : ) :
= Multiset.prod (Multiset.map (fun x => x % n) s) % n
theorem Multiset.sum_int_mod (s : ) (n : ) :
= Multiset.sum (Multiset.map (fun x => x % n) s) % n
theorem Multiset.prod_int_mod (s : ) (n : ) :
= Multiset.prod (Multiset.map (fun x => x % n) s) % n
theorem map_multiset_sum {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {F : Type u_3} [inst : ] (f : F) (s : ) :
f () = Multiset.sum (Multiset.map (f) s)
theorem map_multiset_prod {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {F : Type u_3} [inst : ] (f : F) (s : ) :
f () = Multiset.prod (Multiset.map (f) s)
theorem AddMonoidHom.map_multiset_sum {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : α →+ β) (s : ) :
f () = Multiset.sum (Multiset.map (f) s)
theorem MonoidHom.map_multiset_prod {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : α →* β) (s : ) :
f () = Multiset.prod (Multiset.map (f) s)