English
For a,b in a commutative semiring R and a finite index set ι, the sum over all subsets s⊆ι of a^{|s|} b^{|ι|−|s|} equals (a+b)^{|ι|}.
Русский
Для коммутативной полугруппы R и конечного множества ι сумма по всем подмножествам s⊆ι от a^{|s|} b^{|ι|−|s|} равна (a+b)^{|ι|}.
LaTeX
$$$\\sum_{s\\subseteq \\iota} a^{|s|} b^{|\\iota|-|s|} = (a+b)^{|\\iota|}$$$
Lean4
/-- Summing `a^#s * b^(n-#s)` over all finite subsets `s` of a fintype of cardinality `n`
gives `(a + b)^n`. The "good" proof involves expanding along all coordinates using the fact that
`x^n` is multilinear, but multilinear maps are only available now over rings, so we give instead
a proof reducing to the usual binomial theorem to have a result over semirings. -/
theorem _root_.Fintype.sum_pow_mul_eq_add_pow (ι : Type*) [Fintype ι] (a b : R) :
∑ s : Finset ι, a ^ #s * b ^ (Fintype.card ι - #s) = (a + b) ^ Fintype.card ι :=
Finset.sum_pow_mul_eq_add_pow _ _ _
