no goals
α : Type ?u.35983
β : Type ?u.35986
n : ℕ
R : Type u_1
inst✝ : CommSemiring R
a b : R
⊢ ∑ s : Finset (Fin n), a ^ card s * b ^ (n - card s) = (a + b) ^ n
simpa using Fintype.sum_pow_mul_eq_add_pow (Fin n) a b