monomial_sum_one — Mathlib

English

A single monomial equals the product of the constant polynomial C a and the product of X-powers corresponding to the exponents in s.

Русский

Одиночный моном равен произведению константы C a и произведения X_x^{s_x} по всем x.

LaTeX

$$$\mathrm{monomial}(s) = C(a) \cdot \prod_{x} X_x^{s_x}$$$

Lean4

theorem monomial_sum_one {α : Type*} (s : Finset α) (f : α → σ →₀ ℕ) :
    (monomial (∑ i ∈ s, f i) 1 : MvPolynomial σ R) = ∏ i ∈ s, monomial (f i) 1 :=
  map_prod (monomialOneHom R σ) (fun i => Multiplicative.ofAdd (f i)) s

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