aeval_comp_rename — Mathlib

English

For any σ, τ, R, S with a R-algebra structure on S, the two algebra homomorphisms from MvPolynomial σ R to S given by aeval g ∘ rename k and aeval (g ∘ k) are equal; in other words, (aeval g) ∘ (rename k) = aeval (g ∘ k).

Русский

Пусть существуют структуры алгебр над R; тогда две однозначные гомоморфизмы из MvPolynomial σ R в S, заданные через aeval g после переименования и через aeval (g ∘ k), совпадают: (aeval g) ∘ (rename k) = aeval (g ∘ k).

LaTeX

$$$ (\mathrm{aeval}\ g) \circ (\mathrm{rename}\ k) = \mathrm{MvPolynomial}.\mathrm{aeval} \, (g \circ k) $$$

Lean4

theorem aeval_comp_rename [Algebra R S] : (aeval (R := R) g).comp (rename k) = MvPolynomial.aeval (g ∘ k) :=
  AlgHom.ext fun p ↦ aeval_rename k g p

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