Bundled Hom instances for module and multiplicative actions #
This file defines instances for Module, MulAction and related structures on bundled Hom types.
These are analogous to the instances in Algebra.Module.Pi, but for bundled instead of unbundled
functions.
instance
AddMonoidHom.distribMulAction
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[inst : Monoid R]
[inst : AddMonoid A]
[inst : AddCommMonoid B]
[inst : DistribMulAction R B]
:
DistribMulAction R (A →+ B)
theorem
AddMonoidHom.smul_apply
{R : Type u_3}
{A : Type u_1}
{B : Type u_2}
[inst : Monoid R]
[inst : AddMonoid A]
[inst : AddCommMonoid B]
[inst : DistribMulAction R B]
(r : R)
(f : A →+ B)
(x : A)
:
instance
AddMonoidHom.smulCommClass
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
{B : Type u_4}
[inst : Monoid R]
[inst : Monoid S]
[inst : AddMonoid A]
[inst : AddCommMonoid B]
[inst : DistribMulAction R B]
[inst : DistribMulAction S B]
[inst : SMulCommClass R S B]
:
SMulCommClass R S (A →+ B)
instance
AddMonoidHom.isScalarTower
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
{B : Type u_4}
[inst : Monoid R]
[inst : Monoid S]
[inst : AddMonoid A]
[inst : AddCommMonoid B]
[inst : DistribMulAction R B]
[inst : DistribMulAction S B]
[inst : SMul R S]
[inst : IsScalarTower R S B]
:
IsScalarTower R S (A →+ B)
instance
AddMonoidHom.isCentralScalar
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[inst : Monoid R]
[inst : AddMonoid A]
[inst : AddCommMonoid B]
[inst : DistribMulAction R B]
[inst : DistribMulAction Rᵐᵒᵖ B]
[inst : IsCentralScalar R B]
:
IsCentralScalar R (A →+ B)
instance
AddMonoidHom.module
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[inst : Semiring R]
[inst : AddMonoid A]
[inst : AddCommMonoid B]
[inst : Module R B]
: