# mathlibdocumentation

algebra.big_operators.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.sum_mul {α : Type u} {β : Type v} {s : finset α} {b : β} {f : α → β} [semiring β] :
(∑ (x : α) in s, f x) * b = ∑ (x : α) in s, (f x) * b

theorem finset.mul_sum {α : Type u} {β : Type v} {s : finset α} {b : β} {f : α → β} [semiring β] :
b * ∑ (x : α) in s, f x = ∑ (x : α) in s, b * f x

theorem finset.sum_mul_boole {α : Type u} {β : Type v} [semiring β] [decidable_eq α] (s : finset α) (f : α → β) (a : α) :
∑ (x : α) in s, (f x) * ite (a = x) 1 0 = ite (a s) (f a) 0

theorem finset.sum_boole_mul {α : Type u} {β : Type v} [semiring β] [decidable_eq α] (s : finset α) (f : α → β) (a : α) :
∑ (x : α) in s, (ite (a = x) 1 0) * f x = ite (a s) (f a) 0

theorem finset.sum_div {α : Type u} {β : Type v} {s : finset α} {f : α → β} {b : β} :
(∑ (x : α) in s, f x) / b = ∑ (x : α) in s, f x / b

theorem finset.prod_sum {α : Type u} {β : Type v} {δ : α → Type u_1} [decidable_eq α] [Π (a : α), decidable_eq (δ a)] {s : finset α} {t : Π (a : α), finset (δ a)} {f : Π (a : α), δ a → β} :
∏ (a : α) in s, ∑ (b : δ a) in t a, f a b = ∑ (p : Π (a : α), a sδ a) in s.pi t, ∏ (x : {x // x s}) in s.attach, f x.val (p x.val _)

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.sum_mul_sum {β : Type v} {ι₁ : Type u_1} {ι₂ : Type u_2} (s₁ : finset ι₁) (s₂ : finset ι₂) (f₁ : ι₁ → β) (f₂ : ι₂ → β) :
(∑ (x₁ : ι₁) in s₁, f₁ x₁) * ∑ (x₂ : ι₂) in s₂, f₂ x₂ = ∑ (p : ι₁ × ι₂) in s₁.product s₂, (f₁ p.fst) * f₂ p.snd

theorem finset.prod_add {α : Type u} {β : Type v} (f g : α → β) (s : finset α) :
∏ (a : α) in s, (f a + g a) = ∑ (t : finset α) in s.powerset, (∏ (a : α) in t, f a) * ∏ (a : α) in s \ t, 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.sum_pow_mul_eq_add_pow {α : Type u_1} {R : Type u_2} (a b : R) (s : finset α) :
∑ (t : finset α) in s.powerset, (a ^ t.card) * b ^ (s.card - t.card) = (a + b) ^ s.card

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

theorem finset.prod_pow_eq_pow_sum {α : Type u} {β : Type v} {x : β} {f : α → } {s : finset α} :
∏ (i : α) in s, x ^ f i = x ^ ∑ (x : α) in s, f x

theorem finset.dvd_sum {α : Type u} {β : Type v} {b : β} {s : finset α} {f : α → β} :
(∀ (x : α), x sb f x)b ∑ (x : α) in s, f x

theorem finset.prod_nat_cast {α : Type u} {β : Type v} (s : finset α) (f : α → ) :
∏ (x : α) in s, f x = ∏ (x : α) in s, (f x)

theorem finset.sum_powerset_insert {α : Type u} {β : Type v} [decidable_eq α] {s : finset α} {x : α} (h : x s) (f : → β) :
∑ (a : finset α) in (insert x s).powerset, f a = ∑ (a : finset α) in s.powerset, f a + ∑ (t : finset α) in s.powerset, f (insert x t)

theorem finset.prod_powerset_insert {α : Type u} {β : Type v} [decidable_eq α] [comm_monoid β] {s : finset α} {x : α} (h : x s) (f : → β) :
∏ (a : finset α) in (insert x s).powerset, f a = (∏ (a : finset α) in s.powerset, f a) * ∏ (t : finset α) in s.powerset, 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.