English
If a family of elements x_i in a semiring commute pairwise under multiplication, then the power of their sum expands as a generalized multinomial sum with appropriate combinatorial coefficients.
Русский
Если элементы x_i в полукольце взаимно коммутируют, то степень суммы распадается на обобщённый суммарный мультиномиал с соответствующими комбинаторными коэффициентами.
LaTeX
$$$\left(\sum_{i\in s} x_i\right)^n = \sum_{k\in s.sym(n)} \mathrm{multinomial}(s,k) \; (x_i)^{k_i}$ (с учетом соответствующих правил)$$
Lean4
/-- The **multinomial theorem**. -/
theorem sum_pow_of_commute (x : α → R) (s : Finset α) (hc : (s : Set α).Pairwise (Commute on x)) :
∀ n,
s.sum x ^ n =
∑ k : s.sym n,
k.1.1.multinomial *
(k.1.1.map <| x).noncommProd (Multiset.map_set_pairwise <| hc.mono <| mem_sym_iff.1 k.2) :=
by
induction s using Finset.induction with
| empty =>
rw [sum_empty]
rintro (_ | n)
· rw [_root_.pow_zero, Fintype.sum_subsingleton]
swap
· exact ⟨0, by simp [eq_iff_true_of_subsingleton]⟩
convert (@one_mul R _ _).symm
convert @Nat.cast_one R _
simp
· rw [_root_.pow_succ, mul_zero]
haveI : IsEmpty (Finset.sym (∅ : Finset α) n.succ) := Finset.instIsEmpty
apply (Fintype.sum_empty _).symm
| insert a s ha ih => ?_
intro n; specialize ih (hc.mono <| s.subset_insert a)
rw [sum_insert ha, (Commute.sum_right s _ _ _).add_pow, sum_range]; swap
· exact fun _ hb => hc (mem_insert_self a s) (mem_insert_of_mem hb) (ne_of_mem_of_not_mem hb ha).symm
· simp_rw [ih, mul_sum, sum_mul, sum_sigma', univ_sigma_univ]
refine (Fintype.sum_equiv (symInsertEquiv ha) _ _ fun m => ?_).symm
rw [m.1.1.multinomial_filter_ne a]
conv in m.1.1.map _ => rw [← m.1.1.filter_add_not (a = ·), Multiset.map_add]
simp_rw [Multiset.noncommProd_add, m.1.1.filter_eq, Multiset.map_replicate, m.1.2]
rw [Multiset.noncommProd_eq_pow_card _ _ _ fun _ => Multiset.eq_of_mem_replicate]
rw [Multiset.card_replicate, Nat.cast_mul, mul_assoc, Nat.cast_comm]
congr 1; simp_rw [← mul_assoc, Nat.cast_comm]; rfl
