mathlib documentation

algebra.module.hom

Bundled hom instances for module and multiplicative actions #

This file defines instances for module, mul_action and related structures on bundled _hom types.

These are analogous to the instances in algebra.module.pi, but for bundled instead of unbundled functions.

@[protected, instance]
def add_monoid_hom.distrib_mul_action {R : Type u_1} {A : Type u_3} {B : Type u_4} [monoid R] [add_monoid A] [add_comm_monoid B] [distrib_mul_action R B] :
Equations
@[simp]
theorem add_monoid_hom.coe_smul {R : Type u_1} {A : Type u_3} {B : Type u_4} [monoid R] [add_monoid A] [add_comm_monoid B] [distrib_mul_action R B] (r : R) (f : A →+ B) :
(r f) = r f
theorem add_monoid_hom.smul_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [monoid R] [add_monoid A] [add_comm_monoid B] [distrib_mul_action R B] (r : R) (f : A →+ B) (x : A) :
(r f) x = r f x
@[protected, instance]
def add_monoid_hom.smul_comm_class {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [monoid R] [monoid S] [add_monoid A] [add_comm_monoid B] [distrib_mul_action R B] [distrib_mul_action S B] [smul_comm_class R S B] :
@[protected, instance]
def add_monoid_hom.is_scalar_tower {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [monoid R] [monoid S] [add_monoid A] [add_comm_monoid B] [distrib_mul_action R B] [distrib_mul_action S B] [has_smul R S] [is_scalar_tower R S B] :
@[protected, instance]
def add_monoid_hom.is_central_scalar {R : Type u_1} {A : Type u_3} {B : Type u_4} [monoid R] [add_monoid A] [add_comm_monoid B] [distrib_mul_action R B] [distrib_mul_action Rᵐᵒᵖ B] [is_central_scalar R B] :
@[protected, instance]
def add_monoid_hom.module {R : Type u_1} {A : Type u_3} {B : Type u_4} [semiring R] [add_monoid A] [add_comm_monoid B] [module R B] :
module R (A →+ B)
Equations