instCoeTCNonUnitalAlgHomId — Mathlib

English

For a function-like family F that satisfies the NonUnitalAlgHomClass axioms, there is a canonical way to view F as a NonUnitalAlgHom via the identity R-algebra hom, i.e., a natural coercion F ⇒ (A →ₙₐ[R] B).

Русский

Для функционального семейства F, удовлетворяющего аксиомам NonUnitalAlgHomClass, существует канонический способ рассматривать F как ненулевой алгебропомохомом через тождественное R-алгебраическое отображение.

LaTeX

$$$ \\text{There is a canonical coercion } F \\Rightarrow (A \\to_{n\\_R} B) \\text{ given by the identity on the R-algebra structure.}$$$

Lean4

instance {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] :
    CoeTC F (A →ₙₐ[R] B) :=
  ⟨toNonUnitalAlgHom⟩

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