Action instances for OrderDual #
This file provides instances of algebraic actions for OrderDual. Note that the SMul instances
are already defined in Mathlib.Algebra.Order.Group.Synonym.
See also #
instance
OrderDual.instSMulWithZero
{α : Type u_1}
{β : Type u_2}
[Zero α]
[Zero β]
[SMulWithZero α β]
:
SMulWithZero αᵒᵈ β
Equations
- OrderDual.instSMulWithZero = SMulWithZero.mk ⋯
instance
OrderDual.instSMulWithZero'
{α : Type u_1}
{β : Type u_2}
[Zero α]
[Zero β]
[SMulWithZero α β]
:
SMulWithZero α βᵒᵈ
Equations
- OrderDual.instSMulWithZero' = SMulWithZero.mk ⋯
Equations
- OrderDual.instAddAction = AddAction.mk ⋯ ⋯
Equations
- OrderDual.instMulAction = MulAction.mk ⋯ ⋯
Equations
- OrderDual.instAddAction' = AddAction.mk ⋯ ⋯
Equations
- OrderDual.instMulAction' = MulAction.mk ⋯ ⋯
instance
OrderDual.instVAddCommClass
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[VAdd β γ]
[VAdd α γ]
[VAddCommClass α β γ]
:
VAddCommClass αᵒᵈ β γ
Equations
- ⋯ = inst
instance
OrderDual.instSMulCommClass
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[SMul β γ]
[SMul α γ]
[SMulCommClass α β γ]
:
SMulCommClass αᵒᵈ β γ
Equations
- ⋯ = inst
instance
OrderDual.instVAddCommClass'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[VAdd β γ]
[VAdd α γ]
[VAddCommClass α β γ]
:
VAddCommClass α βᵒᵈ γ
Equations
- ⋯ = inst
instance
OrderDual.instSMulCommClass'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[SMul β γ]
[SMul α γ]
[SMulCommClass α β γ]
:
SMulCommClass α βᵒᵈ γ
Equations
- ⋯ = inst
instance
OrderDual.instVAddCommClass''
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[VAdd β γ]
[VAdd α γ]
[VAddCommClass α β γ]
:
VAddCommClass α β γᵒᵈ
Equations
- ⋯ = inst
instance
OrderDual.instSMulCommClass''
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[SMul β γ]
[SMul α γ]
[SMulCommClass α β γ]
:
SMulCommClass α β γᵒᵈ
Equations
- ⋯ = inst
instance
OrderDual.instVAddAssocClass
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[VAdd α β]
[VAdd β γ]
[VAdd α γ]
[VAddAssocClass α β γ]
:
VAddAssocClass αᵒᵈ β γ
Equations
- ⋯ = inst
instance
OrderDual.instIsScalarTower
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[SMul α β]
[SMul β γ]
[SMul α γ]
[IsScalarTower α β γ]
:
IsScalarTower αᵒᵈ β γ
Equations
- ⋯ = inst
instance
OrderDual.instVAddAssocClass'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[VAdd α β]
[VAdd β γ]
[VAdd α γ]
[VAddAssocClass α β γ]
:
VAddAssocClass α βᵒᵈ γ
Equations
- ⋯ = inst
instance
OrderDual.instIsScalarTower'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[SMul α β]
[SMul β γ]
[SMul α γ]
[IsScalarTower α β γ]
:
IsScalarTower α βᵒᵈ γ
Equations
- ⋯ = inst
instance
OrderDual.instVAddAssocClass''
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[VAdd α β]
[VAdd β γ]
[VAdd α γ]
[VAddAssocClass α β γ]
:
VAddAssocClass α β γᵒᵈ
Equations
- ⋯ = inst
instance
OrderDual.instIsScalarTower''
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[SMul α β]
[SMul β γ]
[SMul α γ]
[IsScalarTower α β γ]
:
IsScalarTower α β γᵒᵈ
Equations
- ⋯ = inst
instance
OrderDual.instMulActionWithZero
{α : Type u_1}
{β : Type u_2}
[MonoidWithZero α]
[AddMonoid β]
[MulActionWithZero α β]
:
Equations
- OrderDual.instMulActionWithZero = let __src := OrderDual.instMulAction; let __src_1 := OrderDual.instSMulWithZero; MulActionWithZero.mk ⋯ ⋯
instance
OrderDual.instMulActionWithZero'
{α : Type u_1}
{β : Type u_2}
[MonoidWithZero α]
[AddMonoid β]
[MulActionWithZero α β]
:
Equations
- OrderDual.instMulActionWithZero' = let __src := OrderDual.instMulAction'; let __src_1 := OrderDual.instSMulWithZero'; MulActionWithZero.mk ⋯ ⋯
instance
OrderDual.instDistribMulAction
{α : Type u_1}
{β : Type u_2}
[MonoidWithZero α]
[AddMonoid β]
[DistribMulAction α β]
:
Equations
- OrderDual.instDistribMulAction = DistribMulAction.mk ⋯ ⋯
instance
OrderDual.instDistribMulAction'
{α : Type u_1}
{β : Type u_2}
[MonoidWithZero α]
[AddMonoid β]
[DistribMulAction α β]
:
Equations
- OrderDual.instDistribMulAction' = DistribMulAction.mk ⋯ ⋯