English
There is a canonical CoeTC instance turning NonUnitalAlgHomClass F R A B into a coercion to NonUnitalAlgHom (MonoidHom.id R) A B; i.e., every such F yields a concrete NonUnitalAlgHom.
Русский
Существует канонический экземпляр CoeTC, переводящий NonUnitalAlgHomClass F R A B в приведение к NonUnitalAlgHom (MonoidHom.id R) A B; то есть каждый такой F задаёт конкретный NonUnitalAlgHom.
LaTeX
$$$ \\text{NonUnUnAlgHomClass} F R A B \\Rightarrow \\text{NonUnitalAlgHom }(MonoidHom.id R) A B $$$
Lean4
/-- Turn an element of a type `F` satisfying `NonUnitalAlgSemiHomClass F φ A B` into an actual
`NonUnitalAlgHom`. This is declared as the default coercion from `F` to `A →ₛₙₐ[φ] B`. -/
@[coe]
def toNonUnitalAlgSemiHom {F R S : Type*} [Monoid R] [Monoid S] {φ : R →* S} {A B : Type*} [NonUnitalNonAssocSemiring A]
[DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S B] [FunLike F A B]
[NonUnitalAlgSemiHomClass F φ A B] (f : F) : A →ₛₙₐ[φ] B :=
{ (f : A →ₙ+* B) with
toFun := f
map_smul' := map_smulₛₗ f }
