monomial_one_eq — Mathlib

English

A monomial with coefficient 1 factors as a product of (X_s) to the corresponding exponents.

Русский

Мономиал с коэффициентом 1 раскладывается как произведение (X_s) с соответствующими степенями.

LaTeX

$$$\\mathrm{MvPowerSeries.monomial}(\\mathrm{e}, 1) = \\prod_s (\\mathrm{X}(s))^{\\mathrm{e}(s)}$$$

Lean4

theorem _root_.MvPowerSeries.monomial_one_eq (e : σ →₀ ℕ) :
    MvPowerSeries.monomial e (1 : R) = e.prod fun s n ↦ (MvPowerSeries.X s) ^ n :=
  by
  simp only [← coe_X, ← coe_pow, ← coe_monomial, monomial_eq, map_one, one_mul]
  simp only [← coeToMvPowerSeries.ringHom_apply, ← map_finsuppProd]

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