toAlgHom_id — Mathlib

English

The algebra-map version of the identity hom is the identity algebra hom.

Русский

Алгебраическое отображение версии идентичного гомоморфизма совпадает с тождественным алгебраическим гомоморфизмом.

LaTeX

$$$\\text{Hom.toAlgHom}(.\\mathrm{id}\\ P) = \\mathrm{AlgHom.id}\\ _ _$$$

Lean4

@[simp]
theorem toAlgHom_id : Hom.toAlgHom (.id P) = AlgHom.id _ _ := by ext1; simp

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