toNonUnitalStarAlgHom — Mathlib

English

From a unital star-algebra homomorphism one obtains a non-unital star-algebra homomorphism by forgetting the unit.

Русский

Из единичного звездно-алгебра-гомоморфизма получается ненулевой звездно-алгебра-гомоморфизм, забывая единицу.

LaTeX

$$$f: A \to⋆ₐ[R] B \Rightarrow f: A \to⋆ₙₐ[R] B$$$

Lean4

/-- A unital morphism of ⋆-algebras is a `NonUnitalStarAlgHom`. -/
def toNonUnitalStarAlgHom (f : A →⋆ₐ[R] B) : A →⋆ₙₐ[R] B :=
  { f with map_smul' := map_smul f }

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