# Documentation

Mathlib.Algebra.BigOperators.Ring

# Results about big operators with values in a (semi)ring #

We prove results about big operators that involve some interaction between multiplicative and additive structures on the values being combined.

theorem Finset.prod_pow_eq_pow_sum {α : Type u} {β : Type v} [] {x : β} {f : α} {s : } :
(Finset.prod s fun i => x ^ f i) = x ^ Finset.sum s fun x => f x
theorem Finset.sum_mul {α : Type u} {β : Type v} {s : } {b : β} {f : αβ} :
(Finset.sum s fun x => f x) * b = Finset.sum s fun x => f x * b
theorem Finset.mul_sum {α : Type u} {β : Type v} {s : } {b : β} {f : αβ} :
(b * Finset.sum s fun x => f x) = Finset.sum s fun x => b * f x
theorem Finset.sum_mul_sum {β : Type v} {ι₁ : Type u_1} {ι₂ : Type u_2} (s₁ : Finset ι₁) (s₂ : Finset ι₂) (f₁ : ι₁β) (f₂ : ι₂β) :
((Finset.sum s₁ fun x₁ => f₁ x₁) * Finset.sum s₂ fun x₂ => f₂ x₂) = Finset.sum (s₁ ×ˢ s₂) fun p => f₁ p.fst * f₂ p.snd
theorem Finset.dvd_sum {α : Type u} {β : Type v} {b : β} {s : } {f : αβ} (h : ∀ (x : α), x sb f x) :
b Finset.sum s fun x => f x
theorem Finset.sum_mul_boole {α : Type u} {β : Type v} [] [] (s : ) (f : αβ) (a : α) :
(Finset.sum s fun x => f x * if a = x then 1 else 0) = if a s then f a else 0
theorem Finset.sum_boole_mul {α : Type u} {β : Type v} [] [] (s : ) (f : αβ) (a : α) :
(Finset.sum s fun x => (if a = x then 1 else 0) * f x) = if a s then f a else 0
theorem Finset.sum_div {α : Type u} {β : Type v} [] {s : } {f : αβ} {b : β} :
(Finset.sum s fun x => f x) / b = Finset.sum s fun x => f x / b
theorem Finset.prod_sum {α : Type u} {β : Type v} [] {δ : αType u_1} [] [(a : α) → DecidableEq (δ a)] {s : } {t : (a : α) → Finset (δ a)} {f : (a : α) → δ aβ} :
(Finset.prod s fun a => Finset.sum (t a) fun b => f a b) = Finset.sum () fun p => Finset.prod () fun x => f (x) (p x (_ : x s))

The product over a sum can be written as a sum over the product of sets, Finset.Pi. Finset.prod_univ_sum is an alternative statement when the product is over univ.

theorem Finset.prod_add {α : Type u} {β : Type v} [] [] (f : αβ) (g : αβ) (s : ) :
(Finset.prod s fun a => f a + g a) = Finset.sum () fun t => (Finset.prod t fun a => f a) * Finset.prod (s \ t) fun a => g a

The product of f a + g a over all of s is the sum over the powerset of s of the product of f over a subset t times the product of g over the complement of t

theorem Finset.prod_add_ordered {ι : Type u_1} {R : Type u_2} [] [] (s : ) (f : ιR) (g : ιR) :
(Finset.prod s fun i => f i + g i) = (Finset.prod s fun i => f i) + Finset.sum s fun i => (g i * Finset.prod (Finset.filter (fun x => x < i) s) fun j => f j + g j) * Finset.prod (Finset.filter (fun j => i < j) s) fun j => f j

∏ i, (f i + g i) = (∏ i, f i) + ∑ i, g i * (∏ j < i, f j + g j) * (∏ j > i, f j).

theorem Finset.prod_sub_ordered {ι : Type u_1} {R : Type u_2} [] [] (s : ) (f : ιR) (g : ιR) :
(Finset.prod s fun i => f i - g i) = (Finset.prod s fun i => f i) - Finset.sum s fun i => (g i * Finset.prod (Finset.filter (fun x => x < i) s) fun j => f j - g j) * Finset.prod (Finset.filter (fun j => i < j) s) fun j => f j

∏ i, (f i - g i) = (∏ i, f i) - ∑ i, g i * (∏ j < i, f j - g j) * (∏ j > i, f j).

theorem Finset.prod_one_sub_ordered {ι : Type u_1} {R : Type u_2} [] [] (s : ) (f : ιR) :
(Finset.prod s fun i => 1 - f i) = 1 - Finset.sum s fun i => f i * Finset.prod (Finset.filter (fun x => x < i) s) fun j => 1 - f j

∏ i, (1 - f i) = 1 - ∑ i, f i * (∏ j < i, 1 - f j). This formula is useful in construction of a partition of unity from a collection of “bump” functions.

theorem Finset.sum_pow_mul_eq_add_pow {α : Type u_1} {R : Type u_2} [] (a : R) (b : R) (s : ) :
(Finset.sum () fun t => a ^ * b ^ ()) = (a + b) ^

Summing a^s.card * b^(n-s.card) over all finite subsets s of a Finset gives (a + b)^s.card.

theorem Finset.prod_natCast {α : Type u} {β : Type v} [] (s : ) (f : α) :
↑(Finset.prod s fun x => f x) = Finset.prod s fun x => ↑(f x)
theorem Finset.prod_range_cast_nat_sub {R : Type u_1} [] (n : ) (k : ) :
(Finset.prod () fun i => n - i) = ↑(Finset.prod () fun i => n - i)
theorem Finset.sum_powerset_insert {α : Type u} {β : Type v} [] [] {s : } {x : α} (h : ¬x s) (f : β) :
(Finset.sum (Finset.powerset (insert x s)) fun a => f a) = (Finset.sum () fun a => f a) + Finset.sum () fun t => f (insert x t)

A sum over all subsets of s ∪ {x} is obtained by summing the sum over all subsets of s, and over all subsets of s to which one adds x.

theorem Finset.prod_powerset_insert {α : Type u} {β : Type v} [] [] {s : } {x : α} (h : ¬x s) (f : β) :
(Finset.prod (Finset.powerset (insert x s)) fun a => f a) = (Finset.prod () fun a => f a) * Finset.prod () fun t => f (insert x t)

A product over all subsets of s ∪ {x} is obtained by multiplying the product over all subsets of s, and over all subsets of s to which one adds x.

theorem Finset.sum_powerset {α : Type u} {β : Type v} [] (s : ) (f : β) :
(Finset.sum () fun t => f t) = Finset.sum (Finset.range ( + 1)) fun j => Finset.sum () fun t => f t

A sum over powerset s is equal to the double sum over sets of subsets of s with card s = k, for k = 1, ..., card s

theorem Finset.prod_powerset {α : Type u} {β : Type v} [] (s : ) (f : β) :
(Finset.prod () fun t => f t) = Finset.prod (Finset.range ( + 1)) fun j => Finset.prod () fun t => f t

A product over powerset s is equal to the double product over sets of subsets of s with card s = k, for k = 1, ..., card s.

theorem Finset.sum_range_succ_mul_sum_range_succ {β : Type v} (n : ) (k : ) (f : β) (g : β) :
((Finset.sum (Finset.range (n + 1)) fun i => f i) * Finset.sum (Finset.range (k + 1)) fun i => g i) = (((Finset.sum () fun i => f i) * Finset.sum () fun i => g i) + f n * Finset.sum () fun i => g i) + (Finset.sum () fun i => f i) * g k + f n * g k