mathlib3 documentation

group_theory.group_action.sum

Sum instances for additive and multiplicative actions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines instances for additive and multiplicative actions on the binary sum type.

See also #

source
@[protected, instance]
def sum.has_smul {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_smul M α] [has_smul M β] :
has_smul M (α ⊕ β)
Equations
source
@[protected, instance]
def sum.has_vadd {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_vadd M α] [has_vadd M β] :
has_vadd M (α ⊕ β)
Equations
source
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
source
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
source
@[simp]
theorem sum.smul_inl {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_smul M α] [has_smul M β] (a : M) (b : α) :
a • sum.inl b = sum.inl (a • b)
source
@[simp]
theorem sum.vadd_inl {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_vadd M α] [has_vadd M β] (a : M) (b : α) :
a +ᵥ sum.inl b = sum.inl (a +ᵥ b)
source
@[simp]
theorem sum.vadd_inr {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_vadd M α] [has_vadd M β] (a : M) (c : β) :
a +ᵥ sum.inr c = sum.inr (a +ᵥ c)
source
@[simp]
theorem sum.smul_inr {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_smul M α] [has_smul M β] (a : M) (c : β) :
a • sum.inr c = sum.inr (a • c)
source
@[simp]
theorem sum.smul_swap {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_smul M α] [has_smul M β] (a : M) (x : α ⊕ β) :
(a • x).swap = a • x.swap
source
@[simp]
theorem sum.vadd_swap {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_vadd M α] [has_vadd M β] (a : M) (x : α ⊕ β) :
(a +ᵥ x).swap = a +ᵥ x.swap
source
@[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 (α ⊕ β)
source
@[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 (α ⊕ β)
source
@[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 (α ⊕ β)
source
@[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 (α ⊕ β)
source
@[protected, instance]
def sum.is_central_vadd {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_vadd M α] [has_vadd M β] [has_vadd Mᵃᵒᵖ α] [has_vadd Mᵃᵒᵖ β] [is_central_vadd M α] [is_central_vadd M β] :
is_central_vadd M (α ⊕ β)
source
@[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 (α ⊕ β)
source
@[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 (α ⊕ β)
source
@[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 (α ⊕ β)
source
@[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 (α ⊕ β)
source
@[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
source
@[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