Option instances for additive and multiplicative actions #
This file defines instances for additive and multiplicative actions on Option
type. Scalar
multiplication is defined by a • some b = some (a • b)
and a • none = none
.
See also #
def
Option.instIsScalarTowerOptionInstVAddOptionInstVAddOption.proof_1
{M : Type u_1}
{N : Type u_2}
{α : Type u_3}
[inst : VAdd M α]
[inst : VAdd N α]
[inst : VAdd M N]
[inst : VAddAssocClass M N α]
:
VAddAssocClass M N (Option α)
Equations
- (_ : VAddAssocClass M N (Option α)) = (_ : VAddAssocClass M N (Option α))
instance
Option.instIsScalarTowerOptionInstVAddOptionInstVAddOption
{M : Type u_1}
{N : Type u_2}
{α : Type u_3}
[inst : VAdd M α]
[inst : VAdd N α]
[inst : VAdd M N]
[inst : VAddAssocClass M N α]
:
VAddAssocClass M N (Option α)
instance
Option.instIsScalarTowerOptionInstSMulOptionInstSMulOption
{M : Type u_1}
{N : Type u_2}
{α : Type u_3}
[inst : SMul M α]
[inst : SMul N α]
[inst : SMul M N]
[inst : IsScalarTower M N α]
:
IsScalarTower M N (Option α)
def
Option.instVAddCommClassOptionInstVAddOptionInstVAddOption.proof_1
{M : Type u_1}
{N : Type u_2}
{α : Type u_3}
[inst : VAdd M α]
[inst : VAdd N α]
[inst : VAddCommClass M N α]
:
VAddCommClass M N (Option α)
Equations
- (_ : VAddCommClass M N (Option α)) = (_ : VAddCommClass M N (Option α))
instance
Option.instVAddCommClassOptionInstVAddOptionInstVAddOption
{M : Type u_1}
{N : Type u_2}
{α : Type u_3}
[inst : VAdd M α]
[inst : VAdd N α]
[inst : VAddCommClass M N α]
:
VAddCommClass M N (Option α)
instance
Option.instSMulCommClassOptionInstSMulOptionInstSMulOption
{M : Type u_1}
{N : Type u_2}
{α : Type u_3}
[inst : SMul M α]
[inst : SMul N α]
[inst : SMulCommClass M N α]
:
SMulCommClass M N (Option α)
def
Option.instIsCentralVAddOptionInstVAddOptionAddOpposite.proof_1
{M : Type u_1}
{α : Type u_2}
[inst : VAdd M α]
[inst : VAdd Mᵃᵒᵖ α]
[inst : IsCentralVAdd M α]
:
IsCentralVAdd M (Option α)
Equations
- (_ : IsCentralVAdd M (Option α)) = (_ : IsCentralVAdd M (Option α))
instance
Option.instIsCentralVAddOptionInstVAddOptionAddOpposite
{M : Type u_1}
{α : Type u_2}
[inst : VAdd M α]
[inst : VAdd Mᵃᵒᵖ α]
[inst : IsCentralVAdd M α]
:
IsCentralVAdd M (Option α)
instance
Option.instIsCentralScalarOptionInstSMulOptionMulOpposite
{M : Type u_1}
{α : Type u_2}
[inst : SMul M α]
[inst : SMul Mᵐᵒᵖ α]
[inst : IsCentralScalar M α]
:
IsCentralScalar M (Option α)
def
Option.instFaithfulVAddOptionInstVAddOption.proof_1
{M : Type u_1}
{α : Type u_2}
[inst : VAdd M α]
[inst : FaithfulVAdd M α]
:
FaithfulVAdd M (Option α)
Equations
- (_ : FaithfulVAdd M (Option α)) = (_ : FaithfulVAdd M (Option α))
instance
Option.instFaithfulVAddOptionInstVAddOption
{M : Type u_1}
{α : Type u_2}
[inst : VAdd M α]
[inst : FaithfulVAdd M α]
:
FaithfulVAdd M (Option α)
instance
Option.instFaithfulSMulOptionInstSMulOption
{M : Type u_1}
{α : Type u_2}
[inst : SMul M α]
[inst : FaithfulSMul M α]
:
FaithfulSMul M (Option α)