instSMulCommClassDistribMulActionHomId

English

There is a MulAction structure on DistribMulActionHom (MonoidHom.id N) A B by DomMulAct M, making the Hom-space a module over DomMulAct M.

Русский

Для DomMulAct M имеется структура MulAction на DistribMulActionHom (MonoidHom.id N) A B, превращающая пространство гомоморфизмов во модуль над DomMulAct M.

LaTeX

$$MulAction (DomMulAct M) (DistribMulActionHom (MonoidHom.id N) A B)$$

Lean4

instance {M' : Type*} [DistribSMul M' A] [SMulCommClass M' N A] [SMulCommClass M M' A] :
    SMulCommClass Mᵈᵐᵃ M'ᵈᵐᵃ (A →+[N] B) :=
  DFunLike.coe_injective.smulCommClass (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)

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