aevalTower_id — Mathlib

English

The evaluation tower with the identity algebra homomorphism is equal to the standard evaluation map aeval.

Русский

Стек aevalTower с тождественным алгебраическим отображением равен обычному отображению aeval.

LaTeX

$$$$ \operatorname{aevalTower}(\mathrm{AlgHom}.id\, S S) = (\operatorname{aeval} : (σ \to S) \rightarrow MvPolynomial(σ,S) \rightarrow_{S} S). $$$$

Lean4

@[simp]
theorem aevalTower_id : aevalTower (AlgHom.id S S) = (aeval : (σ → S) → MvPolynomial σ S →ₐ[S] S) :=
  by
  ext
  simp only [aevalTower_X, aeval_X]

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