aevalTower_id — Mathlib

English

The aevalTower with the identity algebra hom equals the standard aeval: aevalTower (AlgHom.id S S) = aeval.

Русский

С башней aevalTower, использующей идентичный гомоморфизм, получаем обычную aeval: aevalTower (AlgHom.id S S) = aeval.

LaTeX

$$aevalTower (AlgHom.id S S) = aeval$$

Lean4

@[simp]
theorem aevalTower_id : aevalTower (AlgHom.id S S) = aeval :=
  by
  ext s
  simp only [eval_X, aevalTower_X, coe_aeval_eq_eval]

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