toAlgHom_apply — Mathlib

English

For a morphism f: P.Hom P', the underlying function agrees on evaluation whether viewed as an algebra hom or a ring hom.

Русский

Для отображения f: P.Hom P' соответствующая функция совпадает на применении как алгебра-гомоморфизм и как кольцевой гомоморфизм.

LaTeX

$$$f.toAlgHom\\ x = f.toRingHom\\ x$$$

Lean4

@[simp]
theorem toAlgHom_apply [Algebra R S'] [IsScalarTower R R' S'] (f : Hom P P') (x) : f.toAlgHom x = f.toRingHom x :=
  rfl

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