aeval — Mathlib

English

The evaluation map aeval is the unique R-algebra homomorphism from R[X] to A sending X to x.

Русский

Оценивание aeval является единственным R-алгеброобразующим отображением из R[X] в A, отправляющим X в x.

LaTeX

$$$$\exists! \phi:\ R[X] \to_A[R] A\;\text{ such that }\; \phi(X) = x.$$$$

Lean4

/-- Given a valuation `x` of the variable in an `R`-algebra `A`, `aeval R A x` is
the unique `R`-algebra homomorphism from `R[X]` to `A` sending `X` to `x`.

This is a stronger variant of the linear map `Polynomial.leval`. -/
def aeval : R[X] →ₐ[R] A :=
  eval₂AlgHom' (Algebra.ofId _ _) x (Algebra.commutes · _)

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