toNonUnitalStarAlgHom — Mathlib

English

If F is a StarHomClass between A and B, then F is a NonUnitalStarRingHomClass.

Русский

Если F — звездообразный гомоморфизм между A и B, то F — ненулевой звёздный кольцевой гомоморфизм без единицы.

LaTeX

$$$\forall F\;\Big(\text{StarHomClass } F\; A\; B\Big) \Rightarrow \text{NonUnitalStarRingHomClass } F\; A\; B$$$

Lean4

/-- Turn an element of a type `F` satisfying `NonUnitalAlgHomClass F R A B` and `StarHomClass F A B`
into an actual `NonUnitalStarAlgHom`. This is declared as the default coercion from `F` to
`A →⋆ₙₐ[R] B`. -/
@[coe]
def toNonUnitalStarAlgHom [StarHomClass F A B] (f : F) : A →⋆ₙₐ[R] B :=
  { (f : A →ₙₐ[R] B) with map_star' := map_star f }

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