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 #

@[protected, instance]
def option.has_vadd {M : Type u_1} {α : Type u_3} [has_vadd M α] :
Equations
@[protected, instance]
def option.has_smul {M : Type u_1} {α : Type u_3} [has_smul M α] :
Equations
theorem option.smul_def {M : Type u_1} {α : Type u_3} [has_smul M α] (a : M) (x : option α) :
theorem option.vadd_def {M : Type u_1} {α : Type u_3} [has_vadd M α] (a : M) (x : option α) :
@[simp]
theorem option.vadd_none {M : Type u_1} {α : Type u_3} [has_vadd M α] (a : M) :
@[simp]
theorem option.smul_none {M : Type u_1} {α : Type u_3} [has_smul M α] (a : M) :
@[simp]
theorem option.vadd_some {M : Type u_1} {α : Type u_3} [has_vadd M α] (a : M) (b : α) :
@[simp]
theorem option.smul_some {M : Type u_1} {α : Type u_3} [has_smul M α] (a : M) (b : α) :
@[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 α] :
@[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 α] :
@[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 α] :
@[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 α] :
@[protected, instance]
def option.is_central_scalar {M : Type u_1} {α : Type u_3} [has_smul M α] [has_smul Mᵐᵒᵖ α] [is_central_scalar M α] :
@[protected, instance]
def option.is_central_vadd {M : Type u_1} {α : Type u_3} [has_vadd M α] [has_vadd Mᵃᵒᵖ α] [is_central_vadd M α] :
@[protected, instance]
def option.has_faithful_smul {M : Type u_1} {α : Type u_3} [has_smul M α] [has_faithful_smul M α] :
@[protected, instance]
def option.has_faithful_vadd {M : Type u_1} {α : Type u_3} [has_vadd M α] [has_faithful_vadd M α] :
@[protected, instance]
def option.mul_action {M : Type u_1} {α : Type u_3} [monoid M] [mul_action M α] :
Equations