Documentation

Mathlib.Algebra.Order.Module.Synonym

Action instances for `OrderDual` #

This file provides instances of algebraic actions for OrderDual. Note that the SMul instances are already defined in Mathlib.Algebra.Group.OrderSynonym.

See also #

instance OrderDual.instSMulWithZero {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] :

SMulWithZero αᵒᵈ β

Equations

OrderDual.instSMulWithZero = SMulWithZero.mk (_ : ∀ (m : β), 0 • m = 0)

instance OrderDual.instSMulWithZero' {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] :

SMulWithZero α βᵒᵈ

Equations

OrderDual.instSMulWithZero' = SMulWithZero.mk (_ : ∀ (m : β), 0 • m = 0)

instance OrderDual.instAddAction {α : Type u_1} {β : Type u_2} [AddMonoid α] [AddAction α β] :

AddAction αᵒᵈ β

Equations

OrderDual.instAddAction = AddAction.mk (_ : ∀ (b : β), 0 +ᵥ b = b) (_ : ∀ (g₁ g₂ : α) (p : β), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p))

instance OrderDual.instMulAction {α : Type u_1} {β : Type u_2} [Monoid α] [MulAction α β] :

MulAction αᵒᵈ β

Equations

OrderDual.instMulAction = MulAction.mk (_ : ∀ (b : β), 1 • b = b) (_ : ∀ (x y : α) (b : β), (x * y) • b = x • y • b)

instance OrderDual.instAddAction' {α : Type u_1} {β : Type u_2} [AddMonoid α] [AddAction α β] :

AddAction α βᵒᵈ

Equations

OrderDual.instAddAction' = AddAction.mk (_ : ∀ (b : β), 0 +ᵥ b = b) (_ : ∀ (g₁ g₂ : α) (p : β), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p))

instance OrderDual.instMulAction' {α : Type u_1} {β : Type u_2} [Monoid α] [MulAction α β] :

MulAction α βᵒᵈ

Equations

OrderDual.instMulAction' = MulAction.mk (_ : ∀ (b : β), 1 • b = b) (_ : ∀ (x y : α) (b : β), (x * y) • b = x • y • b)

instance OrderDual.instVAddCommClass {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd β γ] [VAdd α γ] [VAddCommClass α β γ] :

VAddCommClass αᵒᵈ β γ

Equations

(_ : VAddCommClass αᵒᵈ β γ) = inst

instance OrderDual.instSMulCommClass {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SMul β γ] [SMul α γ] [SMulCommClass α β γ] :

SMulCommClass αᵒᵈ β γ

Equations

(_ : SMulCommClass αᵒᵈ β γ) = inst

instance OrderDual.instVAddCommClass' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd β γ] [VAdd α γ] [VAddCommClass α β γ] :

VAddCommClass α βᵒᵈ γ

Equations

(_ : VAddCommClass α βᵒᵈ γ) = inst

instance OrderDual.instSMulCommClass' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SMul β γ] [SMul α γ] [SMulCommClass α β γ] :

SMulCommClass α βᵒᵈ γ

Equations

(_ : SMulCommClass α βᵒᵈ γ) = inst

instance OrderDual.instVAddCommClass'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd β γ] [VAdd α γ] [VAddCommClass α β γ] :

VAddCommClass α β γᵒᵈ

Equations

(_ : VAddCommClass α β γᵒᵈ) = inst

instance OrderDual.instSMulCommClass'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SMul β γ] [SMul α γ] [SMulCommClass α β γ] :

SMulCommClass α β γᵒᵈ

Equations

(_ : SMulCommClass α β γᵒᵈ) = inst

instance OrderDual.instVAddAssocClass {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α β] [VAdd β γ] [VAdd α γ] [VAddAssocClass α β γ] :

VAddAssocClass αᵒᵈ β γ

Equations

(_ : VAddAssocClass αᵒᵈ β γ) = inst

instance OrderDual.instIsScalarTower {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SMul α β] [SMul β γ] [SMul α γ] [IsScalarTower α β γ] :

IsScalarTower αᵒᵈ β γ

Equations

(_ : IsScalarTower αᵒᵈ β γ) = inst

instance OrderDual.instVAddAssocClass' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α β] [VAdd β γ] [VAdd α γ] [VAddAssocClass α β γ] :

VAddAssocClass α βᵒᵈ γ

Equations

(_ : VAddAssocClass α βᵒᵈ γ) = inst

instance OrderDual.instIsScalarTower' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SMul α β] [SMul β γ] [SMul α γ] [IsScalarTower α β γ] :

IsScalarTower α βᵒᵈ γ

Equations

(_ : IsScalarTower α βᵒᵈ γ) = inst

instance OrderDual.instVAddAssocClass'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α β] [VAdd β γ] [VAdd α γ] [VAddAssocClass α β γ] :

VAddAssocClass α β γᵒᵈ

Equations

(_ : VAddAssocClass α β γᵒᵈ) = inst

instance OrderDual.instIsScalarTower'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SMul α β] [SMul β γ] [SMul α γ] [IsScalarTower α β γ] :

IsScalarTower α β γᵒᵈ

Equations

(_ : IsScalarTower α β γᵒᵈ) = inst

instance OrderDual.instMulActionWithZero {α : Type u_1} {β : Type u_2} [MonoidWithZero α] [AddMonoid β] [MulActionWithZero α β] :

MulActionWithZero αᵒᵈ β

Equations

OrderDual.instMulActionWithZero = let src := OrderDual.instMulAction; let src_1 := OrderDual.instSMulWithZero; MulActionWithZero.mk (_ : ∀ (a : αᵒᵈ), a • 0 = 0) (_ : ∀ (m : β), 0 • m = 0)

instance OrderDual.instMulActionWithZero' {α : Type u_1} {β : Type u_2} [MonoidWithZero α] [AddMonoid β] [MulActionWithZero α β] :

MulActionWithZero α βᵒᵈ

Equations

OrderDual.instMulActionWithZero' = let src := OrderDual.instMulAction'; let src_1 := OrderDual.instSMulWithZero'; MulActionWithZero.mk (_ : ∀ (a : α), a • 0 = 0) (_ : ∀ (m : βᵒᵈ), 0 • m = 0)

instance OrderDual.instDistribMulAction {α : Type u_1} {β : Type u_2} [MonoidWithZero α] [AddMonoid β] [DistribMulAction α β] :

DistribMulAction αᵒᵈ β

Equations

OrderDual.instDistribMulAction = DistribMulAction.mk (_ : ∀ (a : α), a • 0 = 0) (_ : ∀ (a : α) (b₁ b₂ : β), a • (b₁ + b₂) = a • b₁ + a • b₂)

instance OrderDual.instDistribMulAction' {α : Type u_1} {β : Type u_2} [MonoidWithZero α] [AddMonoid β] [DistribMulAction α β] :

DistribMulAction α βᵒᵈ

Equations

OrderDual.instDistribMulAction' = DistribMulAction.mk (_ : ∀ (a : α), a • 0 = 0) (_ : ∀ (a : α) (b₁ b₂ : β), a • (b₁ + b₂) = a • b₁ + a • b₂)

instance OrderDual.instModule {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] :

Module αᵒᵈ β

Equations

OrderDual.instModule = Module.mk (_ : ∀ (r s : α) (x : β), (r + s) • x = r • x + s • x) (_ : ∀ (m : β), 0 • m = 0)

instance OrderDual.instModule' {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] :

Module α βᵒᵈ

Equations

OrderDual.instModule' = Module.mk (_ : ∀ (r s : α) (x : β), (r + s) • x = r • x + s • x) (_ : ∀ (m : βᵒᵈ), 0 • m = 0)