mathlib3documentation

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.

• group_theory.group_action.pi
• group_theory.group_action.prod
• group_theory.group_action.sigma
• group_theory.group_action.sum
@[protected, instance]
def option.has_vadd {M : Type u_1} {α : Type u_3} [ α] :
(option α)
Equations
@[protected, instance]
def option.has_smul {M : Type u_1} {α : Type u_3} [ α] :
(option α)
Equations
theorem option.smul_def {M : Type u_1} {α : Type u_3} [ α] (a : M) (x : option α) :
a x = x
theorem option.vadd_def {M : Type u_1} {α : Type u_3} [ α] (a : M) (x : option α) :
a +ᵥ x = x
@[simp]
theorem option.vadd_none {M : Type u_1} {α : Type u_3} [ α] (a : M) :
@[simp]
theorem option.smul_none {M : Type u_1} {α : Type u_3} [ α] (a : M) :
@[simp]
theorem option.vadd_some {M : Type u_1} {α : Type u_3} [ α] (a : M) (b : α) :
@[simp]
theorem option.smul_some {M : Type u_1} {α : Type u_3} [ α] (a : M) (b : α) :
@[protected, instance]
def option.vadd_assoc_class {M : Type u_1} {N : Type u_2} {α : Type u_3} [ α] [ α] [ N] [ α] :
(option α)
@[protected, instance]
def option.is_scalar_tower {M : Type u_1} {N : Type u_2} {α : Type u_3} [ α] [ α] [ N] [ α] :
(option α)
@[protected, instance]
def option.vadd_comm_class {M : Type u_1} {N : Type u_2} {α : Type u_3} [ α] [ α] [ α] :
(option α)
@[protected, instance]
def option.smul_comm_class {M : Type u_1} {N : Type u_2} {α : Type u_3} [ α] [ α] [ α] :
(option α)
@[protected, instance]
def option.is_central_scalar {M : Type u_1} {α : Type u_3} [ α] [ α] [ α] :
(option α)
@[protected, instance]
def option.is_central_vadd {M : Type u_1} {α : Type u_3} [ α] [ α] [ α] :
(option α)
@[protected, instance]
def option.has_faithful_smul {M : Type u_1} {α : Type u_3} [ α] [ α] :
(option α)
@[protected, instance]
def option.has_faithful_vadd {M : Type u_1} {α : Type u_3} [ α] [ α] :
(option α)
@[protected, instance]
def option.mul_action {M : Type u_1} {α : Type u_3} [monoid M] [ α] :
(option α)
Equations