prod_dpow — Mathlib

English

A product of divided powers over a finite set s equals the multinomial coefficient times the divided power of the sum.

Русский

Произведение деленных степеней по конечному множеству s равно многомономному коэффициенту, умноженному на деленную степень суммы.

LaTeX

$$$(s.\\mathrm{prod} i \\mapsto hI.dpow(n\\, i)\\ a) = \\mathrm{multinomial}(s,n) \\cdot hI.dpow(s.sum n)\\ a$$$

Lean4

/-- A product of divided powers is a multinomial coefficient times the divided power

[Roby-1965], formula (III') -/
theorem prod_dpow {ι : Type*} {s : Finset ι} {n : ι → ℕ} (ha : a ∈ I) :
    (s.prod fun i ↦ hI.dpow (n i) a) = multinomial s n * hI.dpow (s.sum n) a := by
  classical
    induction s using Finset.induction with
  | empty =>
    simp only [prod_empty, multinomial_empty, cast_one, sum_empty, one_mul]
    rw [hI.dpow_zero ha]
  | insert _ _ hi
    hrec =>
    rw [prod_insert hi, hrec, ← mul_assoc, mul_comm (hI.dpow (n _) a), mul_assoc, hI.mul_dpow ha, ← sum_insert hi, ←
      mul_assoc]
    apply congr_arg₂ _ _ rfl
    rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]
      -- TODO : can probably be simplified using `DividedPowers.exp`

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