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 #

source
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 }
source
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 }
source
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
source
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
source
@[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)
source
@[simp]
theorem Sum.vadd_inl {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] (a : M) (b : α) :
a +ᵥ Sum.inl b = Sum.inl (a +ᵥ b)
source
@[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)
source
@[simp]
theorem Sum.vadd_inr {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] (a : M) (c : β) :
a +ᵥ Sum.inr c = Sum.inr (a +ᵥ c)
source
@[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
source
@[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
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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 β] :
IsCentralScalar M (α ⊕ β)
Equations
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
instance Sum.FaithfulSMulLeft {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] [FaithfulSMul M α] :
FaithfulSMul M (α ⊕ β)
Equations
  • ⋯ = ⋯
source
instance Sum.FaithfulVAddLeft {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] [FaithfulVAdd M α] :
FaithfulVAdd M (α ⊕ β)
Equations
  • ⋯ = ⋯
source
instance Sum.FaithfulSMulRight {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] [FaithfulSMul M β] :
FaithfulSMul M (α ⊕ β)
Equations
  • ⋯ = ⋯
source
instance Sum.FaithfulVAddRight {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] [FaithfulVAdd M β] :
FaithfulVAdd M (α ⊕ β)
Equations
  • ⋯ = ⋯
source
instance Sum.instMulAction {M : Type u_1} {α : Type u_3} {β : Type u_4} {m : Monoid M} [MulAction M α] [MulAction M β] :
MulAction M (α ⊕ β)
Equations
source
instance Sum.instAddAction {M : Type u_1} {α : Type u_3} {β : Type u_4} {m : AddMonoid M} [AddAction M α] [AddAction M β] :
AddAction M (α ⊕ β)
Equations