mathlib3 documentation

group_theory.group_action.option

Option instances for additive and multiplicative actions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
@[protected, instance]
def option.has_vadd {M : Type u_1} {α : Type u_3} [has_vadd M α] :
has_vadd M (option α)
Equations
source
@[protected, instance]
def option.has_smul {M : Type u_1} {α : Type u_3} [has_smul M α] :
has_smul M (option α)
Equations
source
theorem option.smul_def {M : Type u_1} {α : Type u_3} [has_smul M α] (a : M) (x : option α) :
a • x = option.map (has_smul.smul a) x
source
theorem option.vadd_def {M : Type u_1} {α : Type u_3} [has_vadd M α] (a : M) (x : option α) :
a +ᵥ x = option.map (has_vadd.vadd a) x
source
@[simp]
theorem option.vadd_none {M : Type u_1} {α : Type u_3} [has_vadd M α] (a : M) :
a +ᵥ option.none = option.none
source
@[simp]
theorem option.smul_none {M : Type u_1} {α : Type u_3} [has_smul M α] (a : M) :
a • option.none = option.none
source
@[simp]
theorem option.vadd_some {M : Type u_1} {α : Type u_3} [has_vadd M α] (a : M) (b : α) :
a +ᵥ option.some b = option.some (a +ᵥ b)
source
@[simp]
theorem option.smul_some {M : Type u_1} {α : Type u_3} [has_smul M α] (a : M) (b : α) :
a • option.some b = option.some (a • b)
source
@[protected, instance]
def option.vadd_assoc_class {M : Type u_1} {N : Type u_2} {α : Type u_3} [has_vadd M α] [has_vadd N α] [has_vadd M N] [vadd_assoc_class M N α] :
vadd_assoc_class M N (option α)
source
@[protected, instance]
def option.is_scalar_tower {M : Type u_1} {N : Type u_2} {α : Type u_3} [has_smul M α] [has_smul N α] [has_smul M N] [is_scalar_tower M N α] :
is_scalar_tower M N (option α)
source
@[protected, instance]
def option.vadd_comm_class {M : Type u_1} {N : Type u_2} {α : Type u_3} [has_vadd M α] [has_vadd N α] [vadd_comm_class M N α] :
vadd_comm_class M N (option α)
source
@[protected, instance]
def option.smul_comm_class {M : Type u_1} {N : Type u_2} {α : Type u_3} [has_smul M α] [has_smul N α] [smul_comm_class M N α] :
smul_comm_class M N (option α)
source
@[protected, instance]
def option.is_central_scalar {M : Type u_1} {α : Type u_3} [has_smul M α] [has_smul Mᵐᵒᵖ α] [is_central_scalar M α] :
is_central_scalar M (option α)
source
@[protected, instance]
def option.is_central_vadd {M : Type u_1} {α : Type u_3} [has_vadd M α] [has_vadd Mᵃᵒᵖ α] [is_central_vadd M α] :
is_central_vadd M (option α)
source
@[protected, instance]
def option.has_faithful_smul {M : Type u_1} {α : Type u_3} [has_smul M α] [has_faithful_smul M α] :
has_faithful_smul M (option α)
source
@[protected, instance]
def option.has_faithful_vadd {M : Type u_1} {α : Type u_3} [has_vadd M α] [has_faithful_vadd M α] :
has_faithful_vadd M (option α)
source
@[protected, instance]
def option.mul_action {M : Type u_1} {α : Type u_3} [monoid M] [mul_action M α] :
mul_action M (option α)
Equations