monomial_eq — Mathlib

English

A variant form equating the monomial embedding to a product of X_s with semiring powers.

Русский

Вариант формы тождества мономиала через вложение в произведение X_s c степенями.

LaTeX

$$$\\mathrm{MvPowerSeries.monomial}(e, e.prod (n \\mapsto r(s)^{n})) = e.prod_s ( r(s) \\cdot \\mathrmMvPowerSeries.X(s) )^{e(s)}$$$

Lean4

theorem _root_.MvPowerSeries.monomial_eq (e : σ →₀ ℕ) (r : σ → R) :
    MvPowerSeries.monomial e (e.prod (fun s n => r s ^ n)) = e.prod fun s e => (r s • MvPowerSeries.X s) ^ e := by
  rw [MvPowerSeries.prod_smul_X_eq_smul_monomial_one, ← map_smul, smul_eq_mul, mul_one]

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