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