coe_toAlgHom — Mathlib

English

The underlying map of a star-algebra homomorphism, when viewed as an algebra homomorphism, coincides with the original star-algebra homomorphism.

Русский

Пусть есть звездно-алгебра-гомоморфизм; его базовая карта как гомоморфизма алгебры совпадает с данным гомоморфизмом.

LaTeX

$$$(f.toAlgHom : A \to B) = f$$$

Lean4

@[simp]
theorem coe_toAlgHom {f : A →⋆ₐ[R] B} : (f.toAlgHom : A → B) = f :=
  rfl

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