# 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_4} {β : Type u_5} [VAdd M α] [VAdd M β] :
Equations
• Sum.hasVAdd = { vadd := fun (a : M) => Sum.map (fun (x : α) => a +ᵥ x) fun (x : β) => a +ᵥ x }
instance Sum.instSMulSum {M : Type u_1} {α : Type u_4} {β : Type u_5} [SMul M α] [SMul M β] :
SMul M (α β)
Equations
• Sum.instSMulSum = { smul := fun (a : M) => Sum.map (fun (x : α) => a x) fun (x : β) => a x }
theorem Sum.vadd_def {M : Type u_1} {α : Type u_4} {β : Type u_5} [VAdd M α] [VAdd M β] (a : M) (x : α β) :
a +ᵥ x = Sum.map (fun (x : α) => a +ᵥ x) (fun (x : β) => a +ᵥ x) x
theorem Sum.smul_def {M : Type u_1} {α : Type u_4} {β : Type u_5} [SMul M α] [SMul M β] (a : M) (x : α β) :
a x = Sum.map (fun (x : α) => a x) (fun (x : β) => a x) x
@[simp]
theorem Sum.vadd_inl {M : Type u_1} {α : Type u_4} {β : Type u_5} [VAdd M α] [VAdd M β] (a : M) (b : α) :
a +ᵥ = Sum.inl (a +ᵥ b)
@[simp]
theorem Sum.smul_inl {M : Type u_1} {α : Type u_4} {β : Type u_5} [SMul M α] [SMul M β] (a : M) (b : α) :
a = Sum.inl (a b)
@[simp]
theorem Sum.vadd_inr {M : Type u_1} {α : Type u_4} {β : Type u_5} [VAdd M α] [VAdd M β] (a : M) (c : β) :
a +ᵥ = Sum.inr (a +ᵥ c)
@[simp]
theorem Sum.smul_inr {M : Type u_1} {α : Type u_4} {β : Type u_5} [SMul M α] [SMul M β] (a : M) (c : β) :
a = Sum.inr (a c)
@[simp]
theorem Sum.vadd_swap {M : Type u_1} {α : Type u_4} {β : Type u_5} [VAdd M α] [VAdd M β] (a : M) (x : α β) :
Sum.swap (a +ᵥ x) = a +ᵥ
@[simp]
theorem Sum.smul_swap {M : Type u_1} {α : Type u_4} {β : Type u_5} [SMul M α] [SMul M β] (a : M) (x : α β) :
Sum.swap (a x) = a
instance Sum.instIsScalarTowerSumInstSMulSumInstSMulSum {M : Type u_1} {N : Type u_2} {α : Type u_4} {β : Type u_5} [SMul M α] [SMul M β] [SMul N α] [SMul N β] [SMul M N] [] [] :
IsScalarTower M N (α β)
Equations
Equations
instance Sum.instSMulCommClassSumInstSMulSumInstSMulSum {M : Type u_1} {N : Type u_2} {α : Type u_4} {β : Type u_5} [SMul M α] [SMul M β] [SMul N α] [SMul N β] [] [] :
SMulCommClass M N (α β)
Equations
Equations
instance Sum.instIsCentralScalarSumInstSMulSumMulOpposite {M : Type u_1} {α : Type u_4} {β : Type u_5} [SMul M α] [SMul M β] [SMul Mᵐᵒᵖ α] [SMul Mᵐᵒᵖ β] [] [] :
Equations
instance Sum.FaithfulVAddLeft {M : Type u_1} {α : Type u_4} {β : Type u_5} [VAdd M α] [VAdd M β] [] :
Equations
instance Sum.FaithfulSMulLeft {M : Type u_1} {α : Type u_4} {β : Type u_5} [SMul M α] [SMul M β] [] :
FaithfulSMul M (α β)
Equations
instance Sum.FaithfulVAddRight {M : Type u_1} {α : Type u_4} {β : Type u_5} [VAdd M α] [VAdd M β] [] :
Equations
instance Sum.FaithfulSMulRight {M : Type u_1} {α : Type u_4} {β : Type u_5} [SMul M α] [SMul M β] [] :
FaithfulSMul M (α β)
Equations
theorem Sum.instAddActionSum.proof_1 {M : Type u_3} {α : Type u_1} {β : Type u_2} {m : } [] [] (x : α β) :
0 +ᵥ x = x
instance Sum.instAddActionSum {M : Type u_1} {α : Type u_4} {β : Type u_5} {m : } [] [] :