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.

@[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
@[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] :
@[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_scalar R S] [is_scalar_tower R S B] :