English
There is a CoeTC instance turning NonUnitalAlgHomClass F R A B into a coercion to NonUnitalAlgHom; i.e., F elements can be treated as actual homomorphisms.
Русский
Существует instance CoeTC переводящий NonUnitalAlgHomClass F R A B в приведение к NonUnitalAlgHom; то есть элементы F могут рассматриваться как реальные гомоморфизмы.
LaTeX
$$$ \\text{CoeTC } F (A \\toₙₐ[R] B) $$$
Lean4
/-- Turn an element of a type `F` satisfying `NonUnitalAlgHomClass F R A B` into an actual
@[coe]
`NonUnitalAlgHom`. This is declared as the default coercion from `F` to `A →ₛₙₐ[R] B`. -/
def toNonUnitalAlgHom {F R : Type*} [Monoid R] {A B : Type*} [NonUnitalNonAssocSemiring A] [DistribMulAction R A]
[NonUnitalNonAssocSemiring B] [DistribMulAction R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) :
A →ₙₐ[R] B :=
{ (f : A →ₙ+* B) with
toFun := f
map_smul' := map_smulₛₗ f }
