subst_coe — Mathlib

English

For a polynomial p, substitution commutes with polynomial evaluation: subst a p = aeval a p (viewed in the mv-power-series).

Русский

Для полинома p подстановка согласуется с полиномальной оценкой: subst a p = aeval a p.

LaTeX

$$$\\forall p \\in \\mathrm{MvPolynomial}(\\sigma,R),\\; \\operatorname{subst}(a, p^{\\mathrm{toMvPowerSeries}}) = \\operatorname{MvPolynomial.aeval}(a)(p).$$$

Lean4

theorem subst_coe (p : MvPolynomial σ R) : subst (R := R) a p = MvPolynomial.aeval a p :=
  by
  letI : UniformSpace R := ⊥
  letI : UniformSpace S := ⊥
  rw [subst_eq_eval₂, eval₂_coe, MvPolynomial.aeval_def]

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