Documentation

Mathlib.Algebra.GroupWithZero.Action.Hom

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

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

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

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

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

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)

Equations

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