prod_monomial — Mathlib

English

The product over a finite set of monomials equals a monomial with summed degrees and the product of coefficients.

Русский

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

LaTeX

$$$\prod_{i\in s} \mathrm{monomial}(f(i))(g(i)) = \mathrm{monomial}\Big(\sum_{i\in s} f(i)\Big)\big(\prod_{i\in s} g(i)\big)$$$

Lean4

theorem prod_monomial (f : ι → ℕ) (g : ι → R) (s : Finset ι) :
    ∏ i ∈ s, monomial (f i) (g i) = monomial (∑ i ∈ s, f i) (∏ i ∈ s, g i) := by
  simpa [monomial, Finsupp.single_finset_sum] using MvPowerSeries.prod_monomial (fun i ↦ Finsupp.single () (f i)) g s

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