aevalTower_algebraMap — Mathlib

English

For all x in R, the evaluation tower applied to the algebra map from R into MvPolynomial(σ,R) yields g(x).

Русский

Для всех x в R применение aevalTower к алгебраическому отображению из R в MvPolynomial(σ,R) даёт g(x).

LaTeX

$$$$ \operatorname{aevalTower}(g,y)(\operatorname{algebraMap}_{R}(MvPolynomial(\sigma,R))(x)) = g(x). $$$$

Lean4

theorem aevalTower_algebraMap (x : R) : aevalTower g y (algebraMap R (MvPolynomial σ R) x) = g x :=
  eval₂_C _ _ _

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