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.

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.

theorem Multiset.sum.proof_1 {α : Type u_1} [AddCommMonoid α] (x : α) (y : α) (z : α) : x + (y + z) = y + (x + z)

def Multiset.sum {α : Type u_2} [AddCommMonoid α] : Multiset α → α

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

Equations

• Multiset.sum = Multiset.foldr (fun (x x_1 : α) => x + x_1) ⋯ 0

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

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) ⋯ 1

theorem Multiset.sum_eq_foldr {α : Type u_2} [AddCommMonoid α] (s : Multiset α) : Multiset.sum s = Multiset.foldr (fun (x x_1 : α) => x + x_1) ⋯ 0 s

theorem Multiset.prod_eq_foldr {α : Type u_2} [CommMonoid α] (s : Multiset α) : Multiset.prod s = Multiset.foldr (fun (x x_1 : α) => x * x_1) ⋯ 1 s

theorem Multiset.sum_eq_foldl {α : Type u_2} [AddCommMonoid α] (s : Multiset α) : Multiset.sum s = Multiset.foldl (fun (x x_1 : α) => x + x_1) ⋯ 0 s

theorem Multiset.prod_eq_foldl {α : Type u_2} [CommMonoid α] (s : Multiset α) : Multiset.prod s = Multiset.foldl (fun (x x_1 : α) => x * x_1) ⋯ 1 s

@[simp]

theorem Multiset.sum_coe {α : Type u_2} [AddCommMonoid α] (l : List α) : Multiset.sum ↑l = List.sum l

@[simp]

theorem Multiset.prod_coe {α : Type u_2} [CommMonoid α] (l : List α) : Multiset.prod ↑l = List.prod l

@[simp]

theorem Multiset.sum_toList {α : Type u_2} [AddCommMonoid α] (s : Multiset α) : List.sum (Multiset.toList s) = Multiset.sum s

@[simp]

theorem Multiset.prod_toList {α : Type u_2} [CommMonoid α] (s : Multiset α) : List.prod (Multiset.toList s) = Multiset.prod s

@[simp]

theorem Multiset.sum_zero {α : Type u_2} [AddCommMonoid α] : Multiset.sum 0 = 0

@[simp]

theorem Multiset.prod_zero {α : Type u_2} [CommMonoid α] : Multiset.prod 0 = 1

@[simp]

theorem Multiset.sum_cons {α : Type u_2} [AddCommMonoid α] (a : α) (s : Multiset α) : Multiset.sum (a ::ₘ s) = a + Multiset.sum s

@[simp]

theorem Multiset.prod_cons {α : Type u_2} [CommMonoid α] (a : α) (s : Multiset α) : Multiset.prod (a ::ₘ s) = a * Multiset.prod s

@[simp]

theorem Multiset.sum_erase {α : Type u_2} [AddCommMonoid α] {s : Multiset α} {a : α} [DecidableEq α] (h : a ∈ s) : a + Multiset.sum (Multiset.erase s a) = Multiset.sum s

@[simp]

theorem Multiset.prod_erase {α : Type u_2} [CommMonoid α] {s : Multiset α} {a : α} [DecidableEq α] (h : a ∈ s) : a * Multiset.prod (Multiset.erase s a) = Multiset.prod s

@[simp]

theorem Multiset.sum_map_erase {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] {m : Multiset ι} {f : ι → α} [DecidableEq ι] {a : ι} (h : a ∈ m) : f a + Multiset.sum (Multiset.map f (Multiset.erase m a)) = Multiset.sum (Multiset.map f m)

@[simp]

theorem Multiset.prod_map_erase {ι : Type u_1} {α : Type u_2} [CommMonoid α] {m : Multiset ι} {f : ι → α} [DecidableEq ι] {a : ι} (h : a ∈ m) : f a * Multiset.prod (Multiset.map f (Multiset.erase m a)) = Multiset.prod (Multiset.map f m)

@[simp]

theorem Multiset.sum_singleton {α : Type u_2} [AddCommMonoid α] (a : α) : Multiset.sum {a} = a

@[simp]

theorem Multiset.prod_singleton {α : Type u_2} [CommMonoid α] (a : α) : Multiset.prod {a} = a

theorem Multiset.sum_pair {α : Type u_2} [AddCommMonoid α] (a : α) (b : α) : Multiset.sum {a, b} = a + b

theorem Multiset.prod_pair {α : Type u_2} [CommMonoid α] (a : α) (b : α) : Multiset.prod {a, b} = a * b

@[simp]

theorem Multiset.sum_add {α : Type u_2} [AddCommMonoid α] (s : Multiset α) (t : Multiset α) : Multiset.sum (s + t) = Multiset.sum s + Multiset.sum t

@[simp]

theorem Multiset.prod_add {α : Type u_2} [CommMonoid α] (s : Multiset α) (t : Multiset α) : Multiset.prod (s + t) = Multiset.prod s * Multiset.prod t

theorem Multiset.sum_nsmul {α : Type u_2} [AddCommMonoid α] (m : Multiset α) (n : ℕ) : Multiset.sum (n • m) = n • Multiset.sum m

abbrev Multiset.sum_nsmul.match_1 (motive : ℕ → Prop) : ∀ (x : ℕ), (Unit → motive 0) → (∀ (n : ℕ), motive (Nat.succ n)) → motive x

Equations

• ⋯ = ⋯

theorem Multiset.prod_nsmul {α : Type u_2} [CommMonoid α] (m : Multiset α) (n : ℕ) : Multiset.prod (n • m) = Multiset.prod m ^ n

@[simp]

theorem Multiset.sum_replicate {α : Type u_2} [AddCommMonoid α] (n : ℕ) (a : α) : Multiset.sum (Multiset.replicate n a) = n • a

@[simp]

theorem Multiset.prod_replicate {α : Type u_2} [CommMonoid α] (n : ℕ) (a : α) : Multiset.prod (Multiset.replicate n a) = a ^ n

theorem Multiset.sum_map_eq_nsmul_single {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] {m : Multiset ι} {f : ι → α} [DecidableEq ι] (i : ι) (hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 0) : Multiset.sum (Multiset.map f m) = Multiset.count i m • f i

theorem Multiset.prod_map_eq_pow_single {ι : Type u_1} {α : Type u_2} [CommMonoid α] {m : Multiset ι} {f : ι → α} [DecidableEq ι] (i : ι) (hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 1) : Multiset.prod (Multiset.map f m) = f i ^ Multiset.count i m

theorem Multiset.sum_eq_nsmul_single {α : Type u_2} [AddCommMonoid α] {s : Multiset α} [DecidableEq α] (a : α) (h : ∀ (a' : α), a' ≠ a → a' ∈ s → a' = 0) : Multiset.sum s = Multiset.count a s • a

theorem Multiset.prod_eq_pow_single {α : Type u_2} [CommMonoid α] {s : Multiset α} [DecidableEq α] (a : α) (h : ∀ (a' : α), a' ≠ a → a' ∈ s → a' = 1) : Multiset.prod s = a ^ Multiset.count a s

theorem Multiset.sum_eq_zero {α : Type u_2} [AddCommMonoid α] {s : Multiset α} (h : ∀ x ∈ s, x = 0) : Multiset.sum s = 0

theorem Multiset.prod_eq_one {α : Type u_2} [CommMonoid α] {s : Multiset α} (h : ∀ x ∈ s, x = 1) : Multiset.prod s = 1

theorem Multiset.nsmul_count {α : Type u_2} [AddCommMonoid α] {s : Multiset α} [DecidableEq α] (a : α) : Multiset.count a s • a = Multiset.sum (Multiset.filter (Eq a) s)

theorem Multiset.pow_count {α : Type u_2} [CommMonoid α] {s : Multiset α} [DecidableEq α] (a : α) : a ^ Multiset.count a s = Multiset.prod (Multiset.filter (Eq a) s)

theorem Multiset.sum_hom {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset α) {F : Type u_5} [FunLike F α β] [AddMonoidHomClass F α β] (f : F) : Multiset.sum (Multiset.map (⇑f) s) = f (Multiset.sum s)

theorem Multiset.prod_hom {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] (s : Multiset α) {F : Type u_5} [FunLike F α β] [MonoidHomClass F α β] (f : F) : Multiset.prod (Multiset.map (⇑f) s) = f (Multiset.prod s)

theorem Multiset.sum_hom' {ι : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset ι) {F : Type u_5} [FunLike F α β] [AddMonoidHomClass F α β] (f : F) (g : ι → α) : Multiset.sum (Multiset.map (fun (i : ι) => f (g i)) s) = f (Multiset.sum (Multiset.map g s))

theorem Multiset.prod_hom' {ι : Type u_1} {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] (s : Multiset ι) {F : Type u_5} [FunLike F α β] [MonoidHomClass F α β] (f : F) (g : ι → α) : Multiset.prod (Multiset.map (fun (i : ι) => f (g i)) s) = f (Multiset.prod (Multiset.map g s))

theorem Multiset.sum_hom₂ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] (s : Multiset ι) (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_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CommMonoid α] [CommMonoid β] [CommMonoid γ] (s : Multiset ι) (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_1} {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset ι) {r : α → β → Prop} {f : ι → α} {g : ι → β} (h₁ : r 0 0) (h₂ : ∀ ⦃a : ι⦄ ⦃b : α⦄ ⦃c : β⦄, r b c → r (f a + b) (g a + c)) : r (Multiset.sum (Multiset.map f s)) (Multiset.sum (Multiset.map g s))

theorem Multiset.prod_hom_rel {ι : Type u_1} {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] (s : Multiset ι) {r : α → β → Prop} {f : ι → α} {g : ι → β} (h₁ : r 1 1) (h₂ : ∀ ⦃a : ι⦄ ⦃b : α⦄ ⦃c : β⦄, r b c → r (f a * b) (g a * c)) : r (Multiset.prod (Multiset.map f s)) (Multiset.prod (Multiset.map g s))

theorem Multiset.sum_map_zero {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] {m : Multiset ι} : Multiset.sum (Multiset.map (fun (x : ι) => 0) m) = 0

theorem Multiset.prod_map_one {ι : Type u_1} {α : Type u_2} [CommMonoid α] {m : Multiset ι} : Multiset.prod (Multiset.map (fun (x : ι) => 1) m) = 1

@[simp]

theorem Multiset.sum_map_add {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] {m : Multiset ι} {f : ι → α} {g : ι → α} : Multiset.sum (Multiset.map (fun (i : ι) => f i + g i) m) = Multiset.sum (Multiset.map f m) + Multiset.sum (Multiset.map g m)

@[simp]

theorem Multiset.prod_map_mul {ι : Type u_1} {α : Type u_2} [CommMonoid α] {m : Multiset ι} {f : ι → α} {g : ι → α} : Multiset.prod (Multiset.map (fun (i : ι) => f i * g i) m) = Multiset.prod (Multiset.map f m) * Multiset.prod (Multiset.map g m)

theorem Multiset.sum_map_nsmul {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] {m : Multiset ι} {f : ι → α} {n : ℕ} : Multiset.sum (Multiset.map (fun (i : ι) => n • f i) m) = n • Multiset.sum (Multiset.map f m)

theorem Multiset.prod_map_pow {ι : Type u_1} {α : Type u_2} [CommMonoid α] {m : Multiset ι} {f : ι → α} {n : ℕ} : Multiset.prod (Multiset.map (fun (i : ι) => f i ^ n) m) = Multiset.prod (Multiset.map f m) ^ n

theorem Multiset.sum_map_sum_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommMonoid α] (m : Multiset β) (n : Multiset γ) {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_2} {β : Type u_3} {γ : Type u_4} [CommMonoid α] (m : Multiset β) (n : Multiset γ) {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_2} [AddCommMonoid α] (p : α → Prop) (s : Multiset α) (p_mul : ∀ (a b : α), p a → p b → p (a + b)) (p_one : p 0) (p_s : ∀ a ∈ s, p a) : p (Multiset.sum s)

theorem Multiset.prod_induction {α : Type u_2} [CommMonoid α] (p : α → Prop) (s : Multiset α) (p_mul : ∀ (a b : α), p a → p b → p (a * b)) (p_one : p 1) (p_s : ∀ a ∈ s, p a) : p (Multiset.prod s)

theorem Multiset.sum_induction_nonempty {α : Type u_2} [AddCommMonoid α] {s : Multiset α} (p : α → Prop) (p_mul : ∀ (a b : α), p a → p b → p (a + b)) (hs : s ≠ ∅) (p_s : ∀ a ∈ s, p a) : p (Multiset.sum s)

theorem Multiset.prod_induction_nonempty {α : Type u_2} [CommMonoid α] {s : Multiset α} (p : α → Prop) (p_mul : ∀ (a b : α), p a → p b → p (a * b)) (hs : s ≠ ∅) (p_s : ∀ a ∈ s, p a) : p (Multiset.prod s)

theorem Multiset.prod_dvd_prod_of_le {α : Type u_2} [CommMonoid α] {s : Multiset α} {t : Multiset α} (h : s ≤ t) : Multiset.prod s ∣ Multiset.prod t

theorem Multiset.prod_dvd_prod_of_dvd {α : Type u_2} {β : Type u_3} [CommMonoid β] {S : Multiset α} (g1 : α → β) (g2 : α → β) (h : ∀ a ∈ S, g1 a ∣ g2 a) : Multiset.prod (Multiset.map g1 S) ∣ Multiset.prod (Multiset.map g2 S)

def Multiset.sumAddMonoidHom {α : Type u_2} [AddCommMonoid α] : Multiset α →+ α

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

Equations

• Multiset.sumAddMonoidHom = { toZeroHom := { toFun := Multiset.sum, map_zero' := ⋯ }, map_add' := ⋯ }

@[simp]

theorem Multiset.coe_sumAddMonoidHom {α : Type u_2} [AddCommMonoid α] : ⇑Multiset.sumAddMonoidHom = Multiset.sum

theorem Multiset.sum_map_neg' {α : Type u_2} [SubtractionCommMonoid α] (m : Multiset α) : Multiset.sum (Multiset.map Neg.neg m) = -Multiset.sum m

theorem Multiset.prod_map_inv' {α : Type u_2} [DivisionCommMonoid α] (m : Multiset α) : Multiset.prod (Multiset.map Inv.inv m) = (Multiset.prod m)⁻¹

@[simp]

theorem Multiset.sum_map_neg {ι : Type u_1} {α : Type u_2} [SubtractionCommMonoid α] {m : Multiset ι} {f : ι → α} : Multiset.sum (Multiset.map (fun (i : ι) => -f i) m) = -Multiset.sum (Multiset.map f m)

@[simp]

theorem Multiset.prod_map_inv {ι : Type u_1} {α : Type u_2} [DivisionCommMonoid α] {m : Multiset ι} {f : ι → α} : Multiset.prod (Multiset.map (fun (i : ι) => (f i)⁻¹) m) = (Multiset.prod (Multiset.map f m))⁻¹

@[simp]

theorem Multiset.sum_map_sub {ι : Type u_1} {α : Type u_2} [SubtractionCommMonoid α] {m : Multiset ι} {f : ι → α} {g : ι → α} : Multiset.sum (Multiset.map (fun (i : ι) => f i - g i) m) = Multiset.sum (Multiset.map f m) - Multiset.sum (Multiset.map g m)

@[simp]

theorem Multiset.prod_map_div {ι : Type u_1} {α : Type u_2} [DivisionCommMonoid α] {m : Multiset ι} {f : ι → α} {g : ι → α} : Multiset.prod (Multiset.map (fun (i : ι) => f i / g i) m) = Multiset.prod (Multiset.map f m) / Multiset.prod (Multiset.map g m)

theorem Multiset.sum_map_zsmul {ι : Type u_1} {α : Type u_2} [SubtractionCommMonoid α] {m : Multiset ι} {f : ι → α} {n : ℤ} : Multiset.sum (Multiset.map (fun (i : ι) => n • f i) m) = n • Multiset.sum (Multiset.map f m)

theorem Multiset.prod_map_zpow {ι : Type u_1} {α : Type u_2} [DivisionCommMonoid α] {m : Multiset ι} {f : ι → α} {n : ℤ} : Multiset.prod (Multiset.map (fun (i : ι) => f i ^ n) m) = Multiset.prod (Multiset.map f m) ^ n

theorem Multiset.sum_map_mul_left {ι : Type u_1} {α : Type u_2} [NonUnitalNonAssocSemiring α] {a : α} {s : Multiset ι} {f : ι → α} : Multiset.sum (Multiset.map (fun (i : ι) => a * f i) s) = a * Multiset.sum (Multiset.map f s)

theorem Multiset.sum_map_mul_right {ι : Type u_1} {α : Type u_2} [NonUnitalNonAssocSemiring α] {a : α} {s : Multiset ι} {f : ι → α} : Multiset.sum (Multiset.map (fun (i : ι) => f i * a) s) = Multiset.sum (Multiset.map f s) * a

@[simp]

theorem Multiset.sum_map_singleton {α : Type u_2} (s : Multiset α) : Multiset.sum (Multiset.map (fun (a : α) => {a}) s) = s

theorem Multiset.sum_nat_mod (s : Multiset ℕ) (n : ℕ) : Multiset.sum s % n = Multiset.sum (Multiset.map (fun (x : ℕ) => x % n) s) % n

theorem Multiset.prod_nat_mod (s : Multiset ℕ) (n : ℕ) : Multiset.prod s % n = Multiset.prod (Multiset.map (fun (x : ℕ) => x % n) s) % n

theorem Multiset.sum_int_mod (s : Multiset ℤ) (n : ℤ) : Multiset.sum s % n = Multiset.sum (Multiset.map (fun (x : ℤ) => x % n) s) % n

theorem Multiset.prod_int_mod (s : Multiset ℤ) (n : ℤ) : Multiset.prod s % n = Multiset.prod (Multiset.map (fun (x : ℤ) => x % n) s) % n

theorem map_multiset_sum {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {F : Type u_5} [FunLike F α β] [AddMonoidHomClass F α β] (f : F) (s : Multiset α) : f (Multiset.sum s) = Multiset.sum (Multiset.map (⇑f) s)

theorem map_multiset_prod {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {F : Type u_5} [FunLike F α β] [MonoidHomClass F α β] (f : F) (s : Multiset α) : f (Multiset.prod s) = Multiset.prod (Multiset.map (⇑f) s)

theorem AddMonoidHom.map_multiset_sum {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] (f : α →+ β) (s : Multiset α) : f (Multiset.sum s) = Multiset.sum (Multiset.map (⇑f) s)

theorem MonoidHom.map_multiset_prod {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] (f : α →* β) (s : Multiset α) : f (Multiset.prod s) = Multiset.prod (Multiset.map (⇑f) s)