aevalTower_comp_C — Mathlib

English

For any g and y, the composition of the evaluation tower with the constant-coefficient embedding C coincides with g itself.

Русский

Для любых g и y композиция aevalTower g y с отображением C (вставка констант в полиномах) равна g.

LaTeX

$$$$(\operatorname{aevalTower}(g,y) : MvPolynomial(\sigma,R) \rightarrow_{+/*?*/} A) \circ C = g.$$$$

Lean4

@[simp]
theorem aevalTower_comp_C : (aevalTower g y : MvPolynomial σ R →+* A).comp C = g :=
  RingHom.ext <| aevalTower_C _ _

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