Documentation

Mathlib.Algebra.GroupWithZero.Action.Hom

Zero-related instances on group-like morphisms #

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] :
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] :
instance AddMonoidHom.instDistribSMul {M : Type u_1} {A : Type u_3} {B : Type u_4} [AddZeroClass A] [AddCommMonoid B] [DistribSMul M 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] :
Equations