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

• GroupTheory.GroupAction.Pi
• GroupTheory.GroupAction.Prod
• GroupTheory.GroupAction.Sigma
• GroupTheory.GroupAction.Sum

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 }

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

Equations

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance Option.instIsScalarTowerOptionInstVAddOptionInstVAddOption {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

• (_ : VAddAssocClass M N (Option α)) = (_ : VAddAssocClass M N (Option α))

instance Option.instIsScalarTowerOptionInstSMulOptionInstSMulOption {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

• (_ : IsScalarTower M N (Option α)) = (_ : IsScalarTower M N (Option α))

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

Equations

• (_ : VAddCommClass M N (Option α)) = (_ : VAddCommClass M N (Option α))

instance Option.instSMulCommClassOptionInstSMulOptionInstSMulOption {M : Type u_1} {N : Type u_2} {α : Type u_3} [SMul M α] [SMul N α] [SMulCommClass M N α] : SMulCommClass M N (Option α)

Equations

• (_ : SMulCommClass M N (Option α)) = (_ : SMulCommClass M N (Option α))

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

Equations

• (_ : IsCentralVAdd M (Option α)) = (_ : IsCentralVAdd M (Option α))

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

Equations

• (_ : IsCentralScalar M (Option α)) = (_ : IsCentralScalar M (Option α))

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

Equations

• (_ : FaithfulVAdd M (Option α)) = (_ : FaithfulVAdd M (Option α))

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

Equations

• (_ : FaithfulSMul M (Option α)) = (_ : FaithfulSMul M (Option α))

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

Equations

• Option.instMulActionOption = MulAction.mk (_ : ∀ (b : Option α), 1 • b = b) (_ : ∀ (a₁ a₂ : M) (b : Option α), (a₁ * a₂) • b = a₁ • a₂ • b)