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
instance Option.VAdd {M : Type u_1} {α : Type u_3} [VAdd M α] :
VAdd M (Option α)
Equations
  • Option.VAdd = { vadd := fun (a : M) => Option.map fun (x : α) => a +ᵥ x }
source
instance Option.instSMul {M : Type u_1} {α : Type u_3} [SMul M α] :
SMul M (Option α)
Equations
  • Option.instSMul = { smul := fun (a : M) => Option.map fun (x : α) => a • x }
source
theorem Option.vadd_def {M : Type u_1} {α : Type u_3} [VAdd M α] (a : M) (x : Option α) :
a +ᵥ x = Option.map (fun (x : α) => a +ᵥ x) x
source
theorem Option.smul_def {M : Type u_1} {α : Type u_3} [SMul M α] (a : M) (x : Option α) :
a • x = Option.map (fun (x : α) => a • x) x
source
@[simp]
theorem Option.vadd_none {M : Type u_1} {α : Type u_3} [VAdd M α] (a : M) :
a +ᵥ none = none
source
@[simp]
theorem Option.smul_none {M : Type u_1} {α : Type u_3} [SMul M α] (a : M) :
a • none = none
source
@[simp]
theorem Option.vadd_some {M : Type u_1} {α : Type u_3} [VAdd M α] (a : M) (b : α) :
a +ᵥ some b = some (a +ᵥ b)
source
@[simp]
theorem Option.smul_some {M : Type u_1} {α : Type u_3} [SMul M α] (a : M) (b : α) :
a • some b = some (a • b)
source
instance Option.instIsScalarTowerOfVAdd {M : Type u_1} {N : Type u_2} {α : Type u_3} [VAdd M α] [VAdd N α] [VAdd M N] [VAddAssocClass M N α] :
VAddAssocClass M N (Option α)
Equations
  • ⋯ = ⋯
source
instance Option.instIsScalarTowerOfSMul {M : Type u_1} {N : Type u_2} {α : Type u_3} [SMul M α] [SMul N α] [SMul M N] [IsScalarTower M N α] :
IsScalarTower M N (Option α)
Equations
  • ⋯ = ⋯
source
instance Option.instVAddCommClass {M : Type u_1} {N : Type u_2} {α : Type u_3} [VAdd M α] [VAdd N α] [VAddCommClass M N α] :
VAddCommClass M N (Option α)
Equations
  • ⋯ = ⋯
source
instance Option.instSMulCommClass {M : Type u_1} {N : Type u_2} {α : Type u_3} [SMul M α] [SMul N α] [SMulCommClass M N α] :
SMulCommClass M N (Option α)
Equations
  • ⋯ = ⋯
source
instance Option.instIsCentralVAdd {M : Type u_1} {α : Type u_3} [VAdd M α] [VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] :
IsCentralVAdd M (Option α)
Equations
  • ⋯ = ⋯
source
instance Option.instIsCentralScalar {M : Type u_1} {α : Type u_3} [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] :
IsCentralScalar M (Option α)
Equations
  • ⋯ = ⋯
source
instance Option.instFaithfulVAdd {M : Type u_1} {α : Type u_3} [VAdd M α] [FaithfulVAdd M α] :
FaithfulVAdd M (Option α)
Equations
  • ⋯ = ⋯
source
instance Option.instFaithfulSMul {M : Type u_1} {α : Type u_3} [SMul M α] [FaithfulSMul M α] :
FaithfulSMul M (Option α)
Equations
  • ⋯ = ⋯
source
instance Option.instMulAction {M : Type u_1} {α : Type u_3} [Monoid M] [MulAction M α] :
MulAction M (Option α)
Equations