aevalTower_comp_toAlgHom — Mathlib

English

The composition of the evaluation tower with IsScalarTower.toAlgHom is equal to g.

Русский

Сложение aevalTower с IsScalarTower.toAlgHom равно g.

LaTeX

$$$$ (\operatorname{aevalTower}(g,y) \circ (IsScalarTower.toAlgHom S R (MvPolynomial(\sigma,R)))) = g. $$$$

Lean4

@[simp]
theorem aevalTower_comp_toAlgHom : (aevalTower g y).comp (IsScalarTower.toAlgHom S R (MvPolynomial σ R)) = g :=
  AlgHom.coe_ringHom_injective <| aevalTower_comp_algebraMap _ _

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