Finset.sum_pow_of_commute

theorem Finset.sum_pow_of_commute : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) {R : Type u_2} [inst_1 : Semiring R] (x : α → R) (hc : (↑s).Pairwise fun i j => Commute (x i) (x j)) (n : ℕ), s.sum x ^ n = Finset.univ.sum fun k => ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯

The theorem `Finset.sum_pow_of_commute` states that for any finite set `s` of a type `α` with decidable equality and any function `x` from `α` to a semiring `R`, if any two elements of the image of `s` under `x` commute, then the `n`-th power of the sum of the elements in the image of `s` under `x` is equal to the sum over all elements `k` in the universal finite set of the product of the multinomial of `k` and the non-commutative product of the image of `k` under `x`. This theorem is proven by induction on the number of summands. In other words, it is a generalization of the multinomial theorem where the sum is taken over a finite set `s` of elements that commute pairwise.

More concisely: For any finite set `s` of commuting elements from a type `α` with decidable equality and any function `x` from `α` to a semiring `R`, the `n`-th power of the sum of `x` applied to the elements in `s` equals the sum over all `k` in `s` of the multinomial coefficient `k` and the non-commutative product of `x` applied to `k` repeated `k.n` times.