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