Actions by and on order synonyms #
This PR transfers group action instances from a type α to αᵒᵈ and Lex α.
See also #
Mathlib.Algebra.Order.GroupWithZero.Action.SynonymMathlib.Algebra.Order.Module.Synonym
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'
{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''
{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.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'
{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''
{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
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 α)