subst_monomial — Mathlib

English

Substitution of a monomial equals a product expression: subst a (monomial e r) = algebraMap(r) · (e.prod (a s)^n).

Русский

Подстановка мономиала равна произведению: subst a (monomial e r) = algebraMap(r) · (e.prod (a s)^n).

LaTeX

$$$\\operatorname{subst}(a,\\mathrm{monomial}(e)\\, r) = (\\operatorname{algebraMap} R (\\mathrm{MvPowerSeries}_{\\tau S}))\\, r \\,*\\, (e.prod (\\lambda s n. (a s)^n))$$$

Lean4

theorem subst_monomial (ha : HasSubst a) (e : σ →₀ ℕ) (r : R) :
    subst a (monomial e r) = (algebraMap R (MvPowerSeries τ S) r) * (e.prod (fun s n ↦ (a s) ^ n)) := by
  rw [← coe_substAlgHom ha, substAlgHom_monomial]

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