aeval_X_left — Mathlib

English

Let R be a commutative semiring and σ a set of indeterminates. Then the evaluation homomorphism that sends each indeterminate X_i to itself is the identity on the polynomial ring MvPolynomial(σ, R).

Русский

Пусть R — коммутативное полукольцо, σ — множество переменных. Тогда отображение оценки, отправляющее каждую X_i в себя, совпадает с тождественным отображением на кольце MvPolynomial(σ, R).

LaTeX

$$$$ \operatorname{aeval}_X = \mathrm{id}_{MvPolynomial(\sigma,R)} $$$$

Lean4

theorem aeval_X_left : aeval X = AlgHom.id R (MvPolynomial σ R) :=
  (aeval_unique (AlgHom.id R _)).symm

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