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 #

@[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
@[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
theorem sum.smul_def {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_smul M α] [has_smul M β] (a : M) (x : α β) :
theorem sum.vadd_def {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_vadd M α] [has_vadd M β] (a : M) (x : α β) :
@[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)
@[simp]
theorem sum.vadd_inl {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_vadd M α] [has_vadd M β] (a : M) (b : α) :
@[simp]
theorem sum.vadd_inr {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_vadd M α] [has_vadd M β] (a : M) (c : β) :
@[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)
@[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
@[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
@[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 β] :
@[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 β] :
@[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 α] :
@[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 α] :
@[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 β] :
@[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 β] :
@[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
@[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