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_div
{α : Type u}
{β : Type v}
[division_ring β]
{s : finset α}
{f : α → β}
{b : β} :
theorem
finset.prod_sum
{α : Type u}
{β : Type v}
[comm_semiring β]
{δ : α → Type u_1}
[decidable_eq α]
[Π (a : α), decidable_eq (δ a)]
{s : finset α}
{t : Π (a : α), finset (δ a)}
{f : Π (a : α), δ a → β} :
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.
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}
[comm_semiring R]
(a b : R)
(s : finset α) :
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}
[comm_semiring β]
{x : β}
{f : α → ℕ}
{s : finset α} :
theorem
finset.dvd_sum
{α : Type u}
{β : Type v}
[comm_semiring β]
{b : β}
{s : finset α}
{f : α → β} :
theorem
finset.prod_nat_cast
{α : Type u}
{β : Type v}
[comm_semiring β]
(s : finset α)
(f : α → ℕ) :
theorem
finset.sum_powerset_insert
{α : Type u}
{β : Type v}
[decidable_eq α]
[add_comm_monoid β]
{s : finset α}
{x : α}
(h : x ∉ s)
(f : finset α → β) :
theorem
finset.prod_powerset_insert
{α : Type u}
{β : Type v}
[decidable_eq α]
[comm_monoid β]
{s : finset α}
{x : α}
(h : x ∉ s)
(f : finset α → β) :
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.