instCoeTCNonUnitalAlgHomOfNonUnitalAlgSemiHomClass

English

There is a specialized instance providing a canonical CoeTC map from F to NonUnitalAlgHom MonoidHom.id R A B; i.e., a structured coercion for identity base ring.

Русский

Существует специализированный экземпляр, обеспечивающий каноническое CoeTC отображение из F к NonUnitalAlgHom MonoidHom.id R A B; т.е. структурированное приведение для тождественного базового кольца.

LaTeX

$$$ \\text{instCoeTCNonUnUnAlgHomId } F $$$

Lean4

instance {F R S A B : Type*} [Monoid R] [Monoid S] {φ : R →* S} [NonUnitalNonAssocSemiring A] [DistribMulAction R A]
    [NonUnitalNonAssocSemiring B] [DistribMulAction S B] [FunLike F A B] [NonUnitalAlgSemiHomClass F φ A B] :
    CoeTC F (A →ₛₙₐ[φ] B) :=
  ⟨toNonUnitalAlgSemiHom⟩

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