substAlgHom_monomial — Mathlib

English

A restatement of substitution of X: subst a (X s) = a s.

Русский

Повторение подстановки X: subst a (X s) = a s.

LaTeX

$$$\\operatorname{subst}\\ a\\ (X\\,s) = a\\,s$$$

Lean4

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

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