mapAlgHom_id — Mathlib

English

The ring-hom underlying mapAlgHom f coincides with the ordinary map of polynomials induced by f on coefficients.

Русский

Гомоморфизм кольца, лежащий в основе mapAlgHom f, совпадает с обычным отображением полиномов, порождаемым коэффициентами через f.

LaTeX

$$$\\\\text{coe} (mapAlgHom f) = map f$$$

Lean4

@[simp]
theorem mapAlgHom_id [Algebra R S₁] : mapAlgHom (AlgHom.id R S₁) = AlgHom.id R (MvPolynomial σ S₁) :=
  AlgHom.ext map_id

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