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 α β] :
Equations
instance OrderDual.instSMulWithZero' {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMulWithZero α β] :
Equations
instance OrderDual.instAddAction {α : Type u_1} {β : Type u_2} [AddMonoid α] [AddAction α β] :
Equations
instance OrderDual.instMulAction {α : Type u_1} {β : Type u_2} [Monoid α] [MulAction α β] :
Equations
instance OrderDual.instAddAction' {α : Type u_1} {β : Type u_2} [AddMonoid α] [AddAction α β] :
Equations
instance OrderDual.instMulAction' {α : Type u_1} {β : Type u_2} [Monoid α] [MulAction α β] :
Equations
instance OrderDual.instVAddCommClass {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd β γ] [VAdd α γ] [VAddCommClass α β γ] :
Equations
instance OrderDual.instSMulCommClass {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SMul β γ] [SMul α γ] [SMulCommClass α β γ] :
Equations
instance OrderDual.instVAddCommClass' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd β γ] [VAdd α γ] [VAddCommClass α β γ] :
Equations
instance OrderDual.instSMulCommClass' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SMul β γ] [SMul α γ] [SMulCommClass α β γ] :
Equations
instance OrderDual.instVAddCommClass'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd β γ] [VAdd α γ] [VAddCommClass α β γ] :
Equations
instance OrderDual.instSMulCommClass'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SMul β γ] [SMul α γ] [SMulCommClass α β γ] :
Equations
instance OrderDual.instVAddAssocClass {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α β] [VAdd β γ] [VAdd α γ] [VAddAssocClass α β γ] :
Equations
instance OrderDual.instIsScalarTower {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SMul α β] [SMul β γ] [SMul α γ] [IsScalarTower α β γ] :
Equations
instance OrderDual.instVAddAssocClass' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α β] [VAdd β γ] [VAdd α γ] [VAddAssocClass α β γ] :
Equations
instance OrderDual.instIsScalarTower' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SMul α β] [SMul β γ] [SMul α γ] [IsScalarTower α β γ] :
Equations
instance OrderDual.instVAddAssocClass'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α β] [VAdd β γ] [VAdd α γ] [VAddAssocClass α β γ] :
Equations
instance OrderDual.instIsScalarTower'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SMul α β] [SMul β γ] [SMul α γ] [IsScalarTower α β γ] :
Equations
Equations
  • OrderDual.instMulActionWithZero = let src := OrderDual.instMulAction; let src_1 := OrderDual.instSMulWithZero; MulActionWithZero.mk (_ : ∀ (a : αᵒᵈ), a 0 = 0) (_ : ∀ (m : β), 0 m = 0)
Equations
  • OrderDual.instMulActionWithZero' = let src := OrderDual.instMulAction'; let src_1 := OrderDual.instSMulWithZero'; MulActionWithZero.mk (_ : ∀ (a : α), a 0 = 0) (_ : ∀ (m : βᵒᵈ), 0 m = 0)
Equations
Equations
instance OrderDual.instModule {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] :
Equations
instance OrderDual.instModule' {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] :
Equations