Zero-related • instances on group-like morphisms

instance AddMonoidHom.instSMulZeroClassOfDistribSMul {M : Type u_1} {A : Type u_3} {B : Type u_4} [AddZeroClass A] [AddZeroClass B] [DistribSMul M B] : SMulZeroClass M (A →+ B)

theorem AddMonoidHom.coe_smul {M : Type u_1} {A : Type u_3} {B : Type u_4} [AddZeroClass A] [AddZeroClass B] [DistribSMul M B] (m : M) (f : A →+ B) : ⇑(m • f) = m • ⇑f

@[simp]

theorem AddMonoidHom.smul_apply {M : Type u_1} {A : Type u_3} {B : Type u_4} [AddZeroClass A] [AddZeroClass B] [DistribSMul M B] (m : M) (f : A →+ B) (a : A) : (m • f) a = m • f a

theorem AddMonoidHom.smul_comp {M : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [AddZeroClass A] [AddZeroClass B] [AddZeroClass C] [DistribSMul M C] (m : M) (g : B →+ C) (f : A →+ B) : (m • g).comp f = m • g.comp f

instance AddMonoidHom.instSMulCommClass {M : Type u_1} {N : Type u_2} {A : Type u_3} {B : Type u_4} [AddZeroClass A] [AddZeroClass B] [DistribSMul M B] [DistribSMul N B] [SMulCommClass M N B] : SMulCommClass M N (A →+ B)

instance AddMonoidHom.instIsScalarTower {M : Type u_1} {N : Type u_2} {A : Type u_3} {B : Type u_4} [AddZeroClass A] [AddZeroClass B] [SMul M N] [DistribSMul M B] [DistribSMul N B] [IsScalarTower M N B] : IsScalarTower M N (A →+ B)

instance AddMonoidHom.instIsCentralScalar {M : Type u_1} {A : Type u_3} {B : Type u_4} [AddZeroClass A] [AddZeroClass B] [DistribSMul M B] [DistribSMul Mᵐᵒᵖ B] [IsCentralScalar M B] : IsCentralScalar M (A →+ B)

instance AddMonoidHom.instDistribSMul {M : Type u_1} {A : Type u_3} {B : Type u_4} [AddZeroClass A] [AddCommMonoid B] [DistribSMul M B] : DistribSMul M (A →+ B)

instance AddMonoidHom.instDistribMulAction {M : Type u_1} {A : Type u_3} {B : Type u_4} [AddZeroClass A] [AddCommMonoid B] [Monoid M] [DistribMulAction M B] : DistribMulAction M (A →+ B)