Prod instances for additive and multiplicative actions #
This file defines instances for binary product of additive and multiplicative actions
@[protected, instance]
def
prod.has_scalar
{M : Type u_1}
{α : Type u_4}
{β : Type u_5}
[has_scalar M α]
[has_scalar M β] :
has_scalar M (α × β)
@[simp]
theorem
prod.smul_fst
{M : Type u_1}
{α : Type u_4}
{β : Type u_5}
[has_scalar M α]
[has_scalar M β]
(a : M)
(x : α × β) :
@[simp]
theorem
prod.smul_snd
{M : Type u_1}
{α : Type u_4}
{β : Type u_5}
[has_scalar M α]
[has_scalar M β]
(a : M)
(x : α × β) :
@[simp]
theorem
prod.smul_mk
{M : Type u_1}
{α : Type u_4}
{β : Type u_5}
[has_scalar M α]
[has_scalar M β]
(a : M)
(b : α)
(c : β) :
theorem
prod.smul_def
{M : Type u_1}
{α : Type u_4}
{β : Type u_5}
[has_scalar M α]
[has_scalar M β]
(a : M)
(x : α × β) :
@[protected, instance]
def
prod.is_scalar_tower
{M : Type u_1}
{N : Type u_2}
{α : Type u_4}
{β : Type u_5}
[has_scalar M α]
[has_scalar M β]
[has_scalar N α]
[has_scalar N β]
[has_scalar M N]
[is_scalar_tower M N α]
[is_scalar_tower M N β] :
is_scalar_tower M N (α × β)
@[protected, instance]
def
prod.vadd_comm_class
{M : Type u_1}
{N : Type u_2}
{α : Type u_4}
{β : Type u_5}
[has_vadd M α]
[has_vadd M β]
[has_vadd N α]
[has_vadd N β]
[vadd_comm_class M N α]
[vadd_comm_class M N β] :
vadd_comm_class M N (α × β)
@[protected, instance]
def
prod.smul_comm_class
{M : Type u_1}
{N : Type u_2}
{α : Type u_4}
{β : Type u_5}
[has_scalar M α]
[has_scalar M β]
[has_scalar N α]
[has_scalar N β]
[smul_comm_class M N α]
[smul_comm_class M N β] :
smul_comm_class M N (α × β)
@[protected, instance]
def
prod.is_central_scalar
{M : Type u_1}
{α : Type u_4}
{β : Type u_5}
[has_scalar M α]
[has_scalar M β]
[has_scalar Mᵐᵒᵖ α]
[has_scalar Mᵐᵒᵖ β]
[is_central_scalar M α]
[is_central_scalar M β] :
is_central_scalar M (α × β)
@[protected, instance]
def
prod.has_faithful_scalar_left
{M : Type u_1}
{α : Type u_4}
{β : Type u_5}
[has_scalar M α]
[has_scalar M β]
[has_faithful_scalar M α]
[nonempty β] :
has_faithful_scalar M (α × β)
@[protected, instance]
def
prod.has_faithful_vadd_left
{M : Type u_1}
{α : Type u_4}
{β : Type u_5}
[has_vadd M α]
[has_vadd M β]
[has_faithful_vadd M α]
[nonempty β] :
has_faithful_vadd M (α × β)
@[protected, instance]
def
prod.has_faithful_vadd_right
{M : Type u_1}
{α : Type u_4}
{β : Type u_5}
[has_vadd M α]
[has_vadd M β]
[nonempty α]
[has_faithful_vadd M β] :
has_faithful_vadd M (α × β)
@[protected, instance]
def
prod.has_faithful_scalar_right
{M : Type u_1}
{α : Type u_4}
{β : Type u_5}
[has_scalar M α]
[has_scalar M β]
[nonempty α]
[has_faithful_scalar M β] :
has_faithful_scalar M (α × β)
@[protected, instance]
def
prod.vadd_comm_class_both
{M : Type u_1}
{N : Type u_2}
{P : Type u_3}
[add_monoid N]
[add_monoid P]
[has_vadd M N]
[has_vadd M P]
[vadd_comm_class M N N]
[vadd_comm_class M P P] :
vadd_comm_class M (N × P) (N × P)
@[protected, instance]
def
prod.smul_comm_class_both
{M : Type u_1}
{N : Type u_2}
{P : Type u_3}
[monoid N]
[monoid P]
[has_scalar M N]
[has_scalar M P]
[smul_comm_class M N N]
[smul_comm_class M P P] :
smul_comm_class M (N × P) (N × P)
@[protected, instance]
def
prod.is_scalar_tower_both
{M : Type u_1}
{N : Type u_2}
{P : Type u_3}
[monoid N]
[monoid P]
[has_scalar M N]
[has_scalar M P]
[is_scalar_tower M N N]
[is_scalar_tower M P P] :
is_scalar_tower M (N × P) (N × P)
@[protected, instance]
def
prod.add_action
{M : Type u_1}
{α : Type u_4}
{β : Type u_5}
{m : add_monoid M}
[add_action M α]
[add_action M β] :
add_action M (α × β)
Equations
- prod.add_action = {to_has_vadd := prod.has_vadd add_action.to_has_vadd, zero_vadd := _, add_vadd := _}
@[protected, instance]
def
prod.mul_action
{M : Type u_1}
{α : Type u_4}
{β : Type u_5}
{m : monoid M}
[mul_action M α]
[mul_action M β] :
mul_action M (α × β)
Equations
- prod.mul_action = {to_has_scalar := prod.has_scalar mul_action.to_has_scalar, one_smul := _, mul_smul := _}
@[protected, instance]
def
prod.distrib_mul_action
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{r : monoid R}
[add_monoid M]
[add_monoid N]
[distrib_mul_action R M]
[distrib_mul_action R N] :
distrib_mul_action R (M × N)
Equations
@[protected, instance]
def
prod.mul_distrib_mul_action
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{r : monoid R}
[monoid M]
[monoid N]
[mul_distrib_mul_action R M]
[mul_distrib_mul_action R N] :
mul_distrib_mul_action R (M × N)