mathlibdocumentation

group_theory.group_action.sum

Sum instances for additive and multiplicative actions #

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

• group_theory.group_action.option
• group_theory.group_action.pi
• group_theory.group_action.prod
• group_theory.group_action.sigma
@[protected, instance]
def sum.has_smul {M : Type u_1} {α : Type u_4} {β : Type u_5} [ α] [ β] :
β)
Equations
@[protected, instance]
def sum.has_vadd {M : Type u_1} {α : Type u_4} {β : Type u_5} [ α] [ β] :
β)
Equations
theorem sum.smul_def {M : Type u_1} {α : Type u_4} {β : Type u_5} [ α] [ β] (a : M) (x : α β) :
a x = x
theorem sum.vadd_def {M : Type u_1} {α : Type u_4} {β : Type u_5} [ α] [ β] (a : M) (x : α β) :
a +ᵥ x = x
@[simp]
theorem sum.smul_inl {M : Type u_1} {α : Type u_4} {β : Type u_5} [ α] [ β] (a : M) (b : α) :
a = sum.inl (a b)
@[simp]
theorem sum.vadd_inl {M : Type u_1} {α : Type u_4} {β : Type u_5} [ α] [ β] (a : M) (b : α) :
a +ᵥ = sum.inl (a +ᵥ b)
@[simp]
theorem sum.vadd_inr {M : Type u_1} {α : Type u_4} {β : Type u_5} [ α] [ β] (a : M) (c : β) :
a +ᵥ = sum.inr (a +ᵥ c)
@[simp]
theorem sum.smul_inr {M : Type u_1} {α : Type u_4} {β : Type u_5} [ α] [ β] (a : M) (c : β) :
a = sum.inr (a c)
@[simp]
theorem sum.smul_swap {M : Type u_1} {α : Type u_4} {β : Type u_5} [ α] [ β] (a : M) (x : α β) :
(a x).swap = a x.swap
@[simp]
theorem sum.vadd_swap {M : Type u_1} {α : Type u_4} {β : Type u_5} [ α] [ β] (a : M) (x : α β) :
(a +ᵥ x).swap = a +ᵥ x.swap
@[protected, instance]
def sum.is_scalar_tower {M : Type u_1} {N : Type u_2} {α : Type u_4} {β : Type u_5} [ α] [ β] [ α] [ β] [ N] [ α] [ β] :
β)
@[protected, instance]
def sum.smul_comm_class {M : Type u_1} {N : Type u_2} {α : Type u_4} {β : Type u_5} [ α] [ β] [ α] [ β] [ α] [ β] :
β)
@[protected, instance]
def sum.vadd_comm_class {M : Type u_1} {N : Type u_2} {α : Type u_4} {β : Type u_5} [ α] [ β] [ α] [ β] [ α] [ β] :
β)
@[protected, instance]
def sum.is_central_scalar {M : Type u_1} {α : Type u_4} {β : Type u_5} [ α] [ β] [ α] [ β] [ α] [ β] :
β)
@[protected, instance]
def sum.has_faithful_smul_left {M : Type u_1} {α : Type u_4} {β : Type u_5} [ α] [ β] [ α] :
β)
@[protected, instance]
def sum.has_faithful_vadd_left {M : Type u_1} {α : Type u_4} {β : Type u_5} [ α] [ β] [ α] :
β)
@[protected, instance]
def sum.has_faithful_smul_right {M : Type u_1} {α : Type u_4} {β : Type u_5} [ α] [ β] [ β] :
β)
@[protected, instance]
def sum.has_faithful_vadd_right {M : Type u_1} {α : Type u_4} {β : Type u_5} [ α] [ β] [ β] :
β)
@[protected, instance]
def sum.add_action {M : Type u_1} {α : Type u_4} {β : Type u_5} {m : add_monoid M} [ α] [ β] :
β)
Equations
@[protected, instance]
def sum.mul_action {M : Type u_1} {α : Type u_4} {β : Type u_5} {m : monoid M} [ α] [ β] :
β)
Equations