Zero-related • instances on group-like morphisms

@[instance_reducible]

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 := ⋯ }

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

@[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

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

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)

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)

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)

@[instance_reducible]

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 := ⋯ }

@[instance_reducible]

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, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, zero_smul := ⋯ }

@[instance_reducible]

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 := ⋯ }

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_reducible]

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 := ⋯ }

@[instance_reducible]

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, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }