Documentation

Mathlib.Algebra.Module.Hom

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] :
Equations
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) :
↑(r f) x = r f x
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] :
Equations
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] :
Equations
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] :
Module R (A →+ B)
Equations