instSemilinearMapClassOfNonUnitalAlgSemiHomClassToMonoidHomRingHom

English

There is an instance turning NonUnitalAlgHomClass F φ A B into a SemilinearMapClass, given appropriate module structures, ensuring map_smulₛₗ compatibility.

Русский

Существуют экземпляры превращающие NonUnitalAlgHomClass F φ A B в SemilinearMapClass при наличии соответствующих модульных структур, обеспечивая совместимость map_smulₛₗ.

LaTeX

$$$ \\text{SemilinearMapClass } F φ A B $ with $ map_smulₛₗ $$$

Lean4

instance (priority := 100) {F R S A B : Type*} {_ : Semiring R} {_ : Semiring S} {φ : R →+* S} {_ : NonUnitalSemiring A}
    {_ : NonUnitalSemiring B} [Module R A] [Module S B] [FunLike F A B]
    [NonUnitalAlgSemiHomClass (R := R) (S := S) F φ A B] : SemilinearMapClass F φ A B :=
  { ‹NonUnitalAlgSemiHomClass F φ A B› with map_smulₛₗ := map_smulₛₗ }

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