Documentation

Mathlib.Algebra.Group.Action.Sum

Sum instances for additive and multiplicative actions #

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

See also #

instance Sum.hasVAdd {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] :
VAdd M (α β)
Equations
  • Sum.hasVAdd = { vadd := fun (a : M) => Sum.map (fun (x : α) => a +ᵥ x) fun (x : β) => a +ᵥ x }
instance Sum.instSMul {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] :
SMul M (α β)
Equations
  • Sum.instSMul = { smul := fun (a : M) => Sum.map (fun (x : α) => a x) fun (x : β) => a x }
theorem Sum.vadd_def {M : Type u_1} {α : Type u_3} {β : Type u_4} [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_3} {β : Type u_4} [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_3} {β : Type u_4} [VAdd M α] [VAdd M β] (a : M) (b : α) :
@[simp]
theorem Sum.smul_inl {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] (a : M) (b : α) :
a Sum.inl b = Sum.inl (a b)
@[simp]
theorem Sum.vadd_inr {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] (a : M) (c : β) :
@[simp]
theorem Sum.smul_inr {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] (a : M) (c : β) :
a Sum.inr c = Sum.inr (a c)
@[simp]
theorem Sum.vadd_swap {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] (a : M) (x : α β) :
(a +ᵥ x).swap = a +ᵥ x.swap
@[simp]
theorem Sum.smul_swap {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] (a : M) (x : α β) :
(a x).swap = a x.swap
instance Sum.instIsScalarTower {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] [SMul N α] [SMul N β] [SMul M N] [IsScalarTower M N α] [IsScalarTower M N β] :
IsScalarTower M N (α β)
Equations
  • =
instance Sum.instVAddCommClass {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] [VAdd N α] [VAdd N β] [VAddCommClass M N α] [VAddCommClass M N β] :
VAddCommClass M N (α β)
Equations
  • =
instance Sum.instSMulCommClass {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] [SMul N α] [SMul N β] [SMulCommClass M N α] [SMulCommClass M N β] :
SMulCommClass M N (α β)
Equations
  • =
instance Sum.instIsCentralVAdd {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] [VAdd Mᵃᵒᵖ α] [VAdd Mᵃᵒᵖ β] [IsCentralVAdd M α] [IsCentralVAdd M β] :
IsCentralVAdd M (α β)
Equations
  • =
instance Sum.instIsCentralScalar {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] [SMul Mᵐᵒᵖ α] [SMul Mᵐᵒᵖ β] [IsCentralScalar M α] [IsCentralScalar M β] :
Equations
  • =
instance Sum.FaithfulVAddLeft {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] [FaithfulVAdd M α] :
FaithfulVAdd M (α β)
Equations
  • =
instance Sum.FaithfulSMulLeft {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] [FaithfulSMul M α] :
FaithfulSMul M (α β)
Equations
  • =
instance Sum.FaithfulVAddRight {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] [FaithfulVAdd M β] :
FaithfulVAdd M (α β)
Equations
  • =
instance Sum.FaithfulSMulRight {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] [FaithfulSMul M β] :
FaithfulSMul M (α β)
Equations
  • =
instance Sum.instAddAction {M : Type u_1} {α : Type u_3} {β : Type u_4} {m : AddMonoid M} [AddAction M α] [AddAction M β] :
AddAction M (α β)
Equations
theorem Sum.instAddAction.proof_1 {M : Type u_3} {α : Type u_1} {β : Type u_2} {m : AddMonoid M} [AddAction M α] [AddAction M β] (x : α β) :
0 +ᵥ x = x
theorem Sum.instAddAction.proof_2 {M : Type u_3} {α : Type u_1} {β : Type u_2} {m : AddMonoid M} [AddAction M α] [AddAction M β] (a : M) (b : M) (x : α β) :
a + b +ᵥ x = a +ᵥ (b +ᵥ x)
instance Sum.instMulAction {M : Type u_1} {α : Type u_3} {β : Type u_4} {m : Monoid M} [MulAction M α] [MulAction M β] :
MulAction M (α β)
Equations