# Documentation

Mathlib.GroupTheory.GroupAction.Sum

# Sum instances for additive and multiplicative actions #

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

• GroupTheory.GroupAction.Option
• GroupTheory.GroupAction.Pi
• GroupTheory.GroupAction.Prod
• GroupTheory.GroupAction.Sigma
instance Sum.hasVAdd {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] :
Equations
• Sum.hasVAdd = { vadd := fun a => Sum.map ((fun x x_1 => x +ᵥ x_1) a) ((fun x x_1 => x +ᵥ x_1) a) }
instance Sum.instSMulSum {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SMul M α] [inst : SMul M β] :
SMul M (α β)
Equations
• Sum.instSMulSum = { smul := fun a => Sum.map ((fun x x_1 => x x_1) a) ((fun x x_1 => x x_1) a) }
theorem Sum.vadd_def {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : VAdd M α] [inst : VAdd M β] (a : M) (x : α β) :
a +ᵥ x = Sum.map ((fun x x_1 => x +ᵥ x_1) a) ((fun x x_1 => x +ᵥ x_1) a) x
theorem Sum.smul_def {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : SMul M α] [inst : SMul M β] (a : M) (x : α β) :
a x = Sum.map ((fun x x_1 => x x_1) a) ((fun x x_1 => x x_1) a) x
@[simp]
theorem Sum.vadd_inl {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : VAdd M α] [inst : VAdd M β] (a : M) (b : α) :
a +ᵥ = Sum.inl (a +ᵥ b)
@[simp]
theorem Sum.smul_inl {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : SMul M α] [inst : SMul M β] (a : M) (b : α) :
a = Sum.inl (a b)
@[simp]
theorem Sum.vadd_inr {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : VAdd M α] [inst : VAdd M β] (a : M) (c : β) :
a +ᵥ = Sum.inr (a +ᵥ c)
@[simp]
theorem Sum.smul_inr {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : SMul M α] [inst : SMul M β] (a : M) (c : β) :
a = Sum.inr (a c)
@[simp]
theorem Sum.vadd_swap {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : VAdd M α] [inst : VAdd M β] (a : M) (x : α β) :
Sum.swap (a +ᵥ x) = a +ᵥ
@[simp]
theorem Sum.smul_swap {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : SMul M α] [inst : SMul M β] (a : M) (x : α β) :
Sum.swap (a x) = a
instance Sum.instIsScalarTowerSumInstSMulSumInstSMulSum {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [inst : SMul M α] [inst : SMul M β] [inst : SMul N α] [inst : SMul N β] [inst : SMul M N] [inst : ] [inst : ] :
IsScalarTower M N (α β)
Equations
instance Sum.instVAddCommClassSumInstVAddSumInstVAddSum {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd N α] [inst : VAdd N β] [inst : ] [inst : ] :
Equations
def Sum.instVAddCommClassSumInstVAddSumInstVAddSum.proof_1 {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd N α] [inst : VAdd N β] [inst : ] [inst : ] :
Equations
instance Sum.instSMulCommClassSumInstSMulSumInstSMulSum {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [inst : SMul M α] [inst : SMul M β] [inst : SMul N α] [inst : SMul N β] [inst : ] [inst : ] :
SMulCommClass M N (α β)
Equations
def Sum.instIsCentralVAddSumInstVAddSumAddOpposite.proof_1 {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd Mᵃᵒᵖ α] [inst : VAdd Mᵃᵒᵖ β] [inst : ] [inst : ] :
Equations
instance Sum.instIsCentralVAddSumInstVAddSumAddOpposite {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd Mᵃᵒᵖ α] [inst : VAdd Mᵃᵒᵖ β] [inst : ] [inst : ] :
Equations
instance Sum.instIsCentralScalarSumInstSMulSumMulOpposite {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SMul M α] [inst : SMul M β] [inst : SMul Mᵐᵒᵖ α] [inst : SMul Mᵐᵒᵖ β] [inst : ] [inst : ] :
Equations
def Sum.FaithfulVAddLeft.proof_1 {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : ] :
Equations
instance Sum.FaithfulVAddLeft {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : ] :
Equations
instance Sum.FaithfulSMulLeft {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SMul M α] [inst : SMul M β] [inst : ] :
FaithfulSMul M (α β)
Equations
instance Sum.FaithfulVAddRight {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : ] :
Equations
def Sum.FaithfulVAddRight.proof_1 {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : ] :
Equations
instance Sum.FaithfulSMulRight {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SMul M α] [inst : SMul M β] [inst : ] :
FaithfulSMul M (α β)
Equations
def Sum.instAddActionSum.proof_2 {M : Type u_3} {α : Type u_1} {β : Type u_2} {m : } [inst : ] [inst : ] (a : M) (b : M) (x : α β) :
a + b +ᵥ x = a +ᵥ (b +ᵥ x)
Equations
def Sum.instAddActionSum.proof_1 {M : Type u_3} {α : Type u_1} {β : Type u_2} {m : } [inst : ] [inst : ] (x : α β) :
0 +ᵥ x = x
Equations
instance Sum.instAddActionSum {M : Type u_1} {α : Type u_2} {β : Type u_3} {m : } [inst : ] [inst : ] :