toStarAlgHom — Mathlib

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 }

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