aevalTower — Mathlib

English

For the tower construction, aevalTower applied to X_i yields y_i.

Русский

Для конструирования башни aevalTower на X_i получаем y_i.

LaTeX

$$$$ \mathrm{aevalTower}(g,y)(X_i) = y_i $$$$

Lean4

/-- Version of `aeval` for defining algebra homs out of `MvPolynomial σ R` over a smaller base ring
  than `R`. -/
def aevalTower (f : R →ₐ[S] A) (X : σ → A) : MvPolynomial σ R →ₐ[S] A :=
  { eval₂Hom (↑f) X with
    commutes' := fun r => by simp [IsScalarTower.algebraMap_eq S R (MvPolynomial σ R), algebraMap_eq] }

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