Sum instances for additive and multiplicative actions #
This file defines instances for additive and multiplicative actions on the binary sum
type.
See also #
group_theory.group_action.option
group_theory.group_action.pi
group_theory.group_action.prod
group_theory.group_action.sigma
@[protected, instance]
Equations
- sum.has_smul = {smul := λ (a : M), sum.map (has_smul.smul a) (has_smul.smul a)}
@[protected, instance]
Equations
- sum.has_vadd = {vadd := λ (a : M), sum.map (has_vadd.vadd a) (has_vadd.vadd a)}
theorem
sum.smul_def
{M : Type u_1}
{α : Type u_4}
{β : Type u_5}
[has_smul M α]
[has_smul M β]
(a : M)
(x : α ⊕ β) :
a • x = sum.map (has_smul.smul a) (has_smul.smul a) x
theorem
sum.vadd_def
{M : Type u_1}
{α : Type u_4}
{β : Type u_5}
[has_vadd M α]
[has_vadd M β]
(a : M)
(x : α ⊕ β) :
a +ᵥ x = sum.map (has_vadd.vadd a) (has_vadd.vadd a) x
@[protected, instance]
def
sum.is_scalar_tower
{M : Type u_1}
{N : Type u_2}
{α : Type u_4}
{β : Type u_5}
[has_smul M α]
[has_smul M β]
[has_smul N α]
[has_smul N β]
[has_smul M N]
[is_scalar_tower M N α]
[is_scalar_tower M N β] :
is_scalar_tower M N (α ⊕ β)
@[protected, instance]
def
sum.smul_comm_class
{M : Type u_1}
{N : Type u_2}
{α : Type u_4}
{β : Type u_5}
[has_smul M α]
[has_smul M β]
[has_smul N α]
[has_smul N β]
[smul_comm_class M N α]
[smul_comm_class M N β] :
smul_comm_class M N (α ⊕ β)
@[protected, instance]
def
sum.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
sum.is_central_scalar
{M : Type u_1}
{α : Type u_4}
{β : Type u_5}
[has_smul M α]
[has_smul M β]
[has_smul Mᵐᵒᵖ α]
[has_smul Mᵐᵒᵖ β]
[is_central_scalar M α]
[is_central_scalar M β] :
is_central_scalar M (α ⊕ β)
@[protected, instance]
def
sum.has_faithful_smul_left
{M : Type u_1}
{α : Type u_4}
{β : Type u_5}
[has_smul M α]
[has_smul M β]
[has_faithful_smul M α] :
has_faithful_smul M (α ⊕ β)
@[protected, instance]
def
sum.has_faithful_vadd_left
{M : Type u_1}
{α : Type u_4}
{β : Type u_5}
[has_vadd M α]
[has_vadd M β]
[has_faithful_vadd M α] :
has_faithful_vadd M (α ⊕ β)
@[protected, instance]
def
sum.has_faithful_smul_right
{M : Type u_1}
{α : Type u_4}
{β : Type u_5}
[has_smul M α]
[has_smul M β]
[has_faithful_smul M β] :
has_faithful_smul M (α ⊕ β)
@[protected, instance]
def
sum.has_faithful_vadd_right
{M : Type u_1}
{α : Type u_4}
{β : Type u_5}
[has_vadd M α]
[has_vadd M β]
[has_faithful_vadd M β] :
has_faithful_vadd M (α ⊕ β)
@[protected, instance]
def
sum.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
- sum.add_action = {to_has_vadd := sum.has_vadd add_action.to_has_vadd, zero_vadd := _, add_vadd := _}
@[protected, instance]
def
sum.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
- sum.mul_action = {to_has_smul := sum.has_smul mul_action.to_has_smul, one_smul := _, mul_smul := _}