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
.