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

• Mathlib/Algebra/Group/Action/Pi.lean
• Mathlib/Algebra/Group/Action/Sigma.lean
• Mathlib/Algebra/Group/Action/Sum.lean

@[instance_reducible]

instance Option.instSMul_mathlib {M : Type u_1} {α : Type u_3} [SMul M α] : SMul M (Option α)

Equations

• Option.instSMul_mathlib = { smul := fun (a : M) => Option.map fun (x : α) => a • x }

@[instance_reducible]

instance Option.VAdd {M : Type u_1} {α : Type u_3} [_root_.VAdd M α] : _root_.VAdd M (Option α)

Equations

• Option.VAdd = { vadd := fun (a : M) => Option.map fun (x : α) => a +ᵥ x }

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

theorem Option.vadd_def {M : Type u_1} {α : Type u_3} [_root_.VAdd M α] (a : M) (x : Option α) : a +ᵥ x = Option.map (fun (x : α) => a +ᵥ x) x

@[simp]

theorem Option.smul_none {M : Type u_1} {α : Type u_3} [SMul M α] (a : M) : a • none = none

@[simp]

theorem Option.vadd_none {M : Type u_1} {α : Type u_3} [_root_.VAdd M α] (a : M) : a +ᵥ none = none

@[simp]

theorem Option.smul_some {M : Type u_1} {α : Type u_3} [SMul M α] (a : M) (b : α) : a • some b = some (a • b)

@[simp]

theorem Option.vadd_some {M : Type u_1} {α : Type u_3} [_root_.VAdd M α] (a : M) (b : α) : a +ᵥ some b = some (a +ᵥ b)

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 α)

instance Option.instVAddAssocClassOfVAdd {M : Type u_1} {N : Type u_2} {α : Type u_3} [_root_.VAdd M α] [_root_.VAdd N α] [_root_.VAdd M N] [VAddAssocClass M N α] : VAddAssocClass M N (Option α)

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 α)

instance Option.instVAddCommClass {M : Type u_1} {N : Type u_2} {α : Type u_3} [_root_.VAdd M α] [_root_.VAdd N α] [VAddCommClass M N α] : VAddCommClass M N (Option α)

instance Option.instIsCentralScalar {M : Type u_1} {α : Type u_3} [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] : IsCentralScalar M (Option α)

instance Option.instIsCentralVAdd {M : Type u_1} {α : Type u_3} [_root_.VAdd M α] [_root_.VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] : IsCentralVAdd M (Option α)

instance Option.instFaithfulSMul {M : Type u_1} {α : Type u_3} [SMul M α] [FaithfulSMul M α] : FaithfulSMul M (Option α)

instance Option.instFaithfulVAdd {M : Type u_1} {α : Type u_3} [_root_.VAdd M α] [FaithfulVAdd M α] : FaithfulVAdd M (Option α)

@[instance_reducible]

instance Option.instMulAction {M : Type u_1} {α : Type u_3} [Monoid M] [MulAction M α] : MulAction M (Option α)

Equations

• Option.instMulAction = { toSMul := Option.instSMul_mathlib, mul_smul := ⋯, one_smul := ⋯ }