sum_pow — Mathlib

English

For any Multiset m with DecidableEq, its multinomial coincides with the finsupp-based multinomial of its toFinsupp representation.

Русский

Для любого мультимножества m с DecidableEq мультиномиал совпадает с мультиномиалом по представлению toFinsupp.

LaTeX

$$$m.multinomial = (m.toFinsupp).multinomial$$$

Lean4

theorem sum_pow (x : α → R) (n : ℕ) : s.sum x ^ n = ∑ k ∈ s.sym n, k.val.multinomial * (k.val.map x).prod :=
  by
  conv_rhs => rw [← sum_coe_sort]
  convert sum_pow_of_commute x s (fun _ _ _ _ _ ↦ Commute.all ..) n
  rw [Multiset.noncommProd_eq_prod]

Похожие утверждения