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] :
distrib_mul_action R (A →+ B)
@[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) :
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) :
@[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] :
smul_comm_class R S (A →+ 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_scalar R S]
[is_scalar_tower R S B] :
is_scalar_tower R S (A →+ 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] :
is_central_scalar R (A →+ 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] :
Equations
- add_monoid_hom.module = {to_distrib_mul_action := {to_mul_action := distrib_mul_action.to_mul_action add_monoid_hom.distrib_mul_action, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}