# Zero-related `•` instances on group-like morphisms #

source
instance ZeroHom.instSMulZeroClass {M : Type u_1} {A : Type u_3} {B : Type u_4} [Zero A] [Zero B] [SMulZeroClass M B] :
SMulZeroClass M (ZeroHom A B)
Equations

- ZeroHom.instSMulZeroClass = { smul := fun (r : M) (f : ZeroHom A B) => { toFun := fun (a : A) => r • f a, map_zero' := ⋯ }, smul_zero := ⋯ }

source
theorem ZeroHom.coe_smul {M : Type u_1} {A : Type u_3} {B : Type u_4} [Zero A] [Zero B] [SMulZeroClass M B] (m : M) (f : ZeroHom A B) :
⇑(m • f) = m • ⇑f
source
@[simp]
theorem ZeroHom.smul_apply {M : Type u_1} {A : Type u_3} {B : Type u_4} [Zero A] [Zero B] [SMulZeroClass M B] (m : M) (f : ZeroHom A B) (a : A) :
(m • f) a = m • f a
source
theorem ZeroHom.smul_comp {M : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [Zero A] [Zero B] [Zero C] [SMulZeroClass M C] (m : M) (g : ZeroHom B C) (f : ZeroHom A B) :
(m • g).comp f = m • g.comp f
source
instance ZeroHom.instSMulCommClass {M : Type u_1} {N : Type u_2} {A : Type u_3} {B : Type u_4} [Zero A] [Zero B] [SMulZeroClass M B] [SMulZeroClass N B] [SMulCommClass M N B] :
SMulCommClass M N (ZeroHom A B)
source
instance ZeroHom.instIsScalarTower {M : Type u_1} {N : Type u_2} {A : Type u_3} {B : Type u_4} [Zero A] [Zero B] [SMul M N] [SMulZeroClass M B] [SMulZeroClass N B] [IsScalarTower M N B] :
IsScalarTower M N (ZeroHom A B)
source
instance ZeroHom.instIsCentralScalar {M : Type u_1} {A : Type u_3} {B : Type u_4} [Zero A] [Zero B] [SMulZeroClass M B] [SMulZeroClass M ᵐᵒᵖ B] [IsCentralScalar M B] :
IsCentralScalar M (ZeroHom A B)
source
instance ZeroHom.instSMulWithZero {M : Type u_1} {A : Type u_3} {B : Type u_4} [Zero A] [Zero B] [Zero M] [SMulWithZero M B] :
SMulWithZero M (ZeroHom A B)
Equations

- ZeroHom.instSMulWithZero = { toSMulZeroClass := ZeroHom.instSMulZeroClass, zero_smul := ⋯ }

source
instance ZeroHom.instMulActionWithZero {M : Type u_1} {A : Type u_3} {B : Type u_4} [Zero A] [Zero B] [MonoidWithZero M] [MulActionWithZero M B] :
MulActionWithZero M (ZeroHom A B)
Equations

- ZeroHom.instMulActionWithZero = { toSMul := inferInstance.toSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, zero_smul := ⋯ }

source
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)
Equations

- AddMonoidHom.instSMulZeroClassOfDistribSMul = { smul := fun (r : M) (f : A →+ B) => { toFun := fun (a : A) => r • f a, map_zero' := ⋯, map_add' := ⋯ }, smul_zero := ⋯ }

source
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
source
@[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
source
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
source
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)
source
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)
source
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)
source
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)
Equations

- AddMonoidHom.instDistribSMul = { toSMulZeroClass := AddMonoidHom.instSMulZeroClassOfDistribSMul, smul_add := ⋯ }

source
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)
Equations

- AddMonoidHom.instDistribMulAction = { toSMul := inferInstance.toSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }