Documentation

Mathlib.Algebra.Order.Group.Action.Synonym

Actions by and on order synonyms #

This PR transfers group action instances from a type α to αᵒᵈ and Lex α.

See also #

@[implicit_reducible]

instance OrderDual.instMulAction {M : Type u_1} {α : Type u_3} [Monoid M] [h : MulAction M α] :

MulAction Mᵒᵈ α

Equations

OrderDual.instMulAction = { toSMul := OrderDual.instSMul', mul_smul := ⋯, one_smul := ⋯ }

@[implicit_reducible]

instance OrderDual.instAddAction {M : Type u_1} {α : Type u_3} [AddMonoid M] [h : AddAction M α] :

AddAction Mᵒᵈ α

Equations

OrderDual.instAddAction = { toVAdd := OrderDual.instVAdd', add_vadd := ⋯, zero_vadd := ⋯ }

@[implicit_reducible]

instance OrderDual.instMulAction_1 {M : Type u_1} {α : Type u_3} [Monoid M] [h : MulAction M α] :

MulAction M αᵒᵈ

Equations

OrderDual.instMulAction_1 = { toSMul := OrderDual.instSMul, mul_smul := ⋯, one_smul := ⋯ }

@[implicit_reducible]

instance OrderDual.instAddAction_1 {M : Type u_1} {α : Type u_3} [AddMonoid M] [h : AddAction M α] :

AddAction M αᵒᵈ

Equations

OrderDual.instAddAction_1 = { toVAdd := OrderDual.instVAdd, add_vadd := ⋯, zero_vadd := ⋯ }

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

SMulCommClass Mᵒᵈ N α

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

VAddCommClass Mᵒᵈ N α

instance OrderDual.instSMulCommClass_1 {M : Type u_1} {N : Type u_2} {α : Type u_3} [SMul M α] [SMul N α] [SMulCommClass M N α] :

SMulCommClass M Nᵒᵈ α

instance OrderDual.instVAddCommClass_1 {M : Type u_1} {N : Type u_2} {α : Type u_3} [VAdd M α] [VAdd N α] [VAddCommClass M N α] :

VAddCommClass M Nᵒᵈ α

instance OrderDual.instSMulCommClass_2 {M : Type u_1} {N : Type u_2} {α : Type u_3} [SMul M α] [SMul N α] [SMulCommClass M N α] :

SMulCommClass M N αᵒᵈ

instance OrderDual.instVAddCommClass_2 {M : Type u_1} {N : Type u_2} {α : Type u_3} [VAdd M α] [VAdd N α] [VAddCommClass M N α] :

VAddCommClass M N αᵒᵈ

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

IsScalarTower Mᵒᵈ N α

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

VAddAssocClass Mᵒᵈ N α

instance OrderDual.instIsScalarTower_1 {M : Type u_1} {N : Type u_2} {α : Type u_3} [SMul M N] [SMul M α] [SMul N α] [IsScalarTower M N α] :

IsScalarTower M Nᵒᵈ α

instance OrderDual.instVAddAssocClass_1 {M : Type u_1} {N : Type u_2} {α : Type u_3} [VAdd M N] [VAdd M α] [VAdd N α] [VAddAssocClass M N α] :

VAddAssocClass M Nᵒᵈ α

instance OrderDual.instIsScalarTower_2 {M : Type u_1} {N : Type u_2} {α : Type u_3} [SMul M N] [SMul M α] [SMul N α] [IsScalarTower M N α] :

IsScalarTower M N αᵒᵈ

instance OrderDual.instVAddAssocClass_2 {M : Type u_1} {N : Type u_2} {α : Type u_3} [VAdd M N] [VAdd M α] [VAdd N α] [VAddAssocClass M N α] :

VAddAssocClass M N αᵒᵈ

@[implicit_reducible]

instance Lex.instMulAction {M : Type u_1} {α : Type u_3} [Monoid M] [MulAction M α] :

MulAction (Lex M) α

Equations

Lex.instMulAction = inst✝

@[implicit_reducible]

instance Lex.instAddAction {M : Type u_1} {α : Type u_3} [AddMonoid M] [AddAction M α] :

AddAction (Lex M) α

Equations

Lex.instAddAction = inst✝

@[implicit_reducible]

instance Lex.instMulAction' {M : Type u_1} {α : Type u_3} [Monoid M] [MulAction M α] :

MulAction M (Lex α)

Equations

Lex.instMulAction' = inst✝

@[implicit_reducible]

instance Lex.instAddAction' {M : Type u_1} {α : Type u_3} [AddMonoid M] [AddAction M α] :

AddAction M (Lex α)

Equations

Lex.instAddAction' = inst✝

instance Lex.instSMulCommClass {M : Type u_1} {N : Type u_2} {α : Type u_3} [SMul M α] [SMul N α] [SMulCommClass M N α] :

SMulCommClass (Lex M) N α

instance Lex.instVAddCommClass {M : Type u_1} {N : Type u_2} {α : Type u_3} [VAdd M α] [VAdd N α] [VAddCommClass M N α] :

VAddCommClass (Lex M) N α

instance Lex.instSMulCommClass' {M : Type u_1} {N : Type u_2} {α : Type u_3} [SMul M α] [SMul N α] [SMulCommClass M N α] :

SMulCommClass M (Lex N) α

instance Lex.instVAddCommClass' {M : Type u_1} {N : Type u_2} {α : Type u_3} [VAdd M α] [VAdd N α] [VAddCommClass M N α] :

VAddCommClass M (Lex N) α

instance Lex.instSMulCommClass'' {M : Type u_1} {N : Type u_2} {α : Type u_3} [SMul M α] [SMul N α] [SMulCommClass M N α] :

SMulCommClass M N (Lex α)

instance Lex.instVAddCommClass'' {M : Type u_1} {N : Type u_2} {α : Type u_3} [VAdd M α] [VAdd N α] [VAddCommClass M N α] :

VAddCommClass M N (Lex α)

instance Lex.instIsScalarTower {M : Type u_1} {N : Type u_2} {α : Type u_3} [SMul M N] [SMul M α] [SMul N α] [IsScalarTower M N α] :

IsScalarTower (Lex M) N α

instance Lex.instVAddAssocClass {M : Type u_1} {N : Type u_2} {α : Type u_3} [VAdd M N] [VAdd M α] [VAdd N α] [VAddAssocClass M N α] :

VAddAssocClass (Lex M) N α

instance Lex.instIsScalarTower' {M : Type u_1} {N : Type u_2} {α : Type u_3} [SMul M N] [SMul M α] [SMul N α] [IsScalarTower M N α] :

IsScalarTower M (Lex N) α

instance Lex.instVAddAssocClass' {M : Type u_1} {N : Type u_2} {α : Type u_3} [VAdd M N] [VAdd M α] [VAdd N α] [VAddAssocClass M N α] :

VAddAssocClass M (Lex N) α

instance Lex.instIsScalarTower'' {M : Type u_1} {N : Type u_2} {α : Type u_3} [SMul M N] [SMul M α] [SMul N α] [IsScalarTower M N α] :

IsScalarTower M N (Lex α)

instance Lex.instVAddAssocClass'' {M : Type u_1} {N : Type u_2} {α : Type u_3} [VAdd M N] [VAdd M α] [VAdd N α] [VAddAssocClass M N α] :

VAddAssocClass M N (Lex α)