Documentation

Mathlib.GroupTheory.GroupAction.Option

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 #

source
ink
instance Option.VAdd {M : Type u_1} {α : Type u_2} [inst : VAdd M α] :
VAdd M (Option α)
Equations
source
ink
instance Option.instSMulOption {M : Type u_1} {α : Type u_2} [inst : SMul M α] :
SMul M (Option α)
Equations
  • Option.instSMulOption = { smul := fun a => Option.map fun x => a • x }
source
ink
theorem Option.vadd_def {M : Type u_2} {α : Type u_1} [inst : VAdd M α] (a : M) (x : Option α) :
a +ᵥ x = Option.map ((fun x x_1 => x +ᵥ x_1) a) x
source
ink
theorem Option.smul_def {M : Type u_2} {α : Type u_1} [inst : SMul M α] (a : M) (x : Option α) :
a • x = Option.map ((fun x x_1 => x • x_1) a) x
source
ink
@[simp]
theorem Option.vadd_none {M : Type u_2} {α : Type u_1} [inst : VAdd M α] (a : M) :
a +ᵥ none = none
source
ink
@[simp]
theorem Option.smul_none {M : Type u_2} {α : Type u_1} [inst : SMul M α] (a : M) :
a • none = none
source
ink
@[simp]
theorem Option.vadd_some {M : Type u_2} {α : Type u_1} [inst : VAdd M α] (a : M) (b : α) :
a +ᵥ some b = some (a +ᵥ b)
source
ink
@[simp]
theorem Option.smul_some {M : Type u_2} {α : Type u_1} [inst : SMul M α] (a : M) (b : α) :
a • some b = some (a • b)
source
ink
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
source
ink
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 α)
Equations
source
ink
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 α)
Equations
source
ink
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
source
ink
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 α)
Equations
source
ink
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 α)
Equations
source
ink
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
source
ink
instance Option.instIsCentralVAddOptionInstVAddOptionAddOpposite {M : Type u_1} {α : Type u_2} [inst : VAdd M α] [inst : VAdd Mᵃᵒᵖ α] [inst : IsCentralVAdd M α] :
IsCentralVAdd M (Option α)
Equations
source
ink
instance Option.instIsCentralScalarOptionInstSMulOptionMulOpposite {M : Type u_1} {α : Type u_2} [inst : SMul M α] [inst : SMul Mᵐᵒᵖ α] [inst : IsCentralScalar M α] :
IsCentralScalar M (Option α)
Equations
source
ink
def Option.instFaithfulVAddOptionInstVAddOption.proof_1 {M : Type u_1} {α : Type u_2} [inst : VAdd M α] [inst : FaithfulVAdd M α] :
FaithfulVAdd M (Option α)
Equations
source
ink
instance Option.instFaithfulVAddOptionInstVAddOption {M : Type u_1} {α : Type u_2} [inst : VAdd M α] [inst : FaithfulVAdd M α] :
FaithfulVAdd M (Option α)
Equations
source
ink
instance Option.instFaithfulSMulOptionInstSMulOption {M : Type u_1} {α : Type u_2} [inst : SMul M α] [inst : FaithfulSMul M α] :
FaithfulSMul M (Option α)
Equations
source
ink
instance Option.instMulActionOption {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst : MulAction M α] :
MulAction M (Option α)
Equations