Sum instances for additive and multiplicative actions #
This file defines instances for additive and multiplicative actions on the binary Sum type.
See also #
@[implicit_reducible]
instance
Sum.instSMul
{M : Type u_1}
{α : Type u_3}
{β : Type u_4}
[SMul M α]
[SMul M β]
:
SMul M (α ⊕ β)
@[implicit_reducible]
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.smul_inl
{M : Type u_1}
{α : Type u_3}
{β : Type u_4}
[SMul M α]
[SMul M β]
(a : M)
(b : α)
:
a • inl b = inl (a • b)
@[simp]
@[simp]
theorem
Sum.smul_inr
{M : Type u_1}
{α : Type u_3}
{β : Type u_4}
[SMul M α]
[SMul M β]
(a : M)
(c : β)
:
a • inr c = inr (a • c)
@[simp]
@[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
@[simp]
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 (α ⊕ β)
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 (α ⊕ β)
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 (α ⊕ β)
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 (α ⊕ β)
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 (α ⊕ β)
instance
Sum.FaithfulSMulLeft
{M : Type u_1}
{α : Type u_3}
{β : Type u_4}
[SMul M α]
[SMul M β]
[FaithfulSMul M α]
:
FaithfulSMul M (α ⊕ β)
instance
Sum.FaithfulVAddLeft
{M : Type u_1}
{α : Type u_3}
{β : Type u_4}
[VAdd M α]
[VAdd M β]
[FaithfulVAdd M α]
:
FaithfulVAdd M (α ⊕ β)
instance
Sum.FaithfulSMulRight
{M : Type u_1}
{α : Type u_3}
{β : Type u_4}
[SMul M α]
[SMul M β]
[FaithfulSMul M β]
:
FaithfulSMul M (α ⊕ β)
instance
Sum.FaithfulVAddRight
{M : Type u_1}
{α : Type u_3}
{β : Type u_4}
[VAdd M α]
[VAdd M β]
[FaithfulVAdd M β]
:
FaithfulVAdd M (α ⊕ β)
@[implicit_reducible]
@[implicit_reducible]