English
Let I be an ideal of a commutative semiring A with a given structure of divided powers. For a finite index set s and elements x_i ∈ I (i ∈ s), the divided power of the sum equals a multinomial-type combination of divided powers of the summands, with no binomial coefficients appearing. Precisely, for all n ≥ 0,\nD_n(∑_{i∈s} x_i) = ∑_{k∈s^{⟂n}} ∏_{i∈s} D_{count_i(k)}(x_i),\nwhere D denotes the divided power operator and count_i(k) is the multiplicity of i in k.
Русский
Пусть I — идеал в коммутативном полупрудке A, оснащённый системой делённых степеней. Для конечного множества индексов s и элементов x_i ∈ I (i ∈ s) делённая степень суммы равна сумме по разложению n между слагаемыми по аналогии с мультиномиалом, без коэффициентов мультиномов. Точно: для любого n≥0,\nD_n(∑_{i∈s} x_i) = ∑_{k∈s.sym n} ∏_{i∈s} D_{Multiset.count i k}(x_i).
LaTeX
$$$\\text{Let }I\\text{ be an ideal of a commutative semiring }A\\text{ with a divisive powers structure }h_I.\\quad\\forall n\\in\\mathbb{N},\\ \\forall s\\text{ finite},\\ x: s\\to A,\\ hx \\in I:\\n h_I.dpow\\,n\\,(s.sum x) \\,=\\, (s.sym\\,n).sum\\!\\;\\\n \\ (k \\mapsto s.prod\\ (\\lambda i, h_I.dpow(\\mathrm{Multiset.count}\,i\\,k)\; (x i)))$$$
Lean4
/-- A “multinomial” theorem for divided powers — without multinomial coefficients -/
theorem dpow_sum {ι : Type*} [DecidableEq ι] {s : Finset ι} {x : ι → A} (hx : ∀ i ∈ s, x i ∈ I) {n : ℕ} :
hI.dpow n (s.sum x) = (s.sym n).sum fun k ↦ s.prod fun i ↦ hI.dpow (Multiset.count i k) (x i) :=
dpow_sum' hI.dpow hI.dpow_zero hI.dpow_add hI.dpow_eval_zero hx
