English
Given an AlgHom f : A →ₐ[R] B, Polynomial.mapAlgHom f is the AlgHom from Polynomial A to Polynomial B that maps each coefficient by f, i.e., it applies f to every coefficient of a polynomial.
Русский
Задан AlgHom f : A →ₐ[R] B, полиномный гомоморфизм Polynomial.mapAlgHom f — это AlgHom от Polynomial A к Polynomial B, который отображает каждый коэффициент через f, то есть применяет f к каждому коэффициенту полинома.
LaTeX
$$Polynomial.mapAlgHom f : Polynomial A →ₐ[R] Polynomial B$$
Lean4
/-- `Polynomial.map` as an `AlgHom` for noncommutative algebras.
This is the algebra version of `Polynomial.mapRingHom`. -/
def mapAlgHom (f : A →ₐ[R] B) : Polynomial A →ₐ[R] Polynomial B
where
toRingHom := mapRingHom f.toRingHom
commutes' := by simp
