English
From an F carrying AlgHomClass and StarHomClass, we obtain a StarAlgHom via a canonical construction.
Русский
Из F с AlgHomClass и StarHomClass получаем StarAlgHom через каноническое построение.
LaTeX
$$toStarAlgHom(f) : A →⋆ₐ[R] B$$
Lean4
/-- Turn an element of a type `F` satisfying `AlgHomClass F R A B` and `StarHomClass F A B` into an
actual `StarAlgHom`. This is declared as the default coercion from `F` to `A →⋆ₐ[R] B`. -/
@[coe]
def toStarAlgHom (f : F) : A →⋆ₐ[R] B :=
{ (f : A →ₐ[R] B) with map_star' := map_star f }