aevalTower_comp_algebraMap — Mathlib

English

The composition of the evaluation tower with the algebra-map from R to MvPolynomial(σ,R) equals the algebra map g.

Русский

Сочетание aevalTower c алгебраическим отображением из R в MvPolynomial(σ,R) равно отображению g.

LaTeX

$$$$ (\operatorname{aevalTower}(g,y) : MvPolynomial(\sigma,R) \rightarrow A) \circ (\operatorname{algebraMap}_{R}(MvPolynomial(\sigma,R))) = g. $$$$

Lean4

theorem aevalTower_comp_algebraMap :
    (aevalTower g y : MvPolynomial σ R →+* A).comp (algebraMap R (MvPolynomial σ R)) = g :=
  aevalTower_comp_C _ _

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