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.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 β]
:
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
- ⋯ = ⋯