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)
:
@[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)
:
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)
:
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
- AddMonoidHom.instDistribSMul = { toSMulZeroClass := AddMonoidHom.instSMulZeroClassOfDistribSMul, smul_add := ⋯ }
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 := ⋯ }