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 #

source
instance OrderDual.instAddAction {M : Type u_1} {α : Type u_3} [AddMonoid M] [AddAction M α] :
AddAction Mᵒᵈ α
Equations
  • OrderDual.instAddAction = inst
source
instance OrderDual.instMulAction {M : Type u_1} {α : Type u_3} [Monoid M] [MulAction M α] :
MulAction Mᵒᵈ α
Equations
  • OrderDual.instMulAction = inst
source
instance OrderDual.instAddAction' {M : Type u_1} {α : Type u_3} [AddMonoid M] [AddAction M α] :
AddAction M αᵒᵈ
Equations
  • OrderDual.instAddAction' = inst
source
instance OrderDual.instMulAction' {M : Type u_1} {α : Type u_3} [Monoid M] [MulAction M α] :
MulAction M αᵒᵈ
Equations
  • OrderDual.instMulAction' = inst
source
instance OrderDual.instVAddCommClass {M : Type u_1} {N : Type u_2} {α : Type u_3} [VAdd M α] [VAdd N α] [VAddCommClass M N α] :
VAddCommClass Mᵒᵈ N α
Equations
  • ⋯ = inst
source
instance OrderDual.instSMulCommClass {M : Type u_1} {N : Type u_2} {α : Type u_3} [SMul M α] [SMul N α] [SMulCommClass M N α] :
SMulCommClass Mᵒᵈ N α
Equations
  • ⋯ = inst
source
instance OrderDual.instVAddCommClass' {M : Type u_1} {N : Type u_2} {α : Type u_3} [VAdd M α] [VAdd N α] [VAddCommClass M N α] :
VAddCommClass M Nᵒᵈ α
Equations
  • ⋯ = inst
source
instance OrderDual.instSMulCommClass' {M : Type u_1} {N : Type u_2} {α : Type u_3} [SMul M α] [SMul N α] [SMulCommClass M N α] :
SMulCommClass M Nᵒᵈ α
Equations
  • ⋯ = inst
source
instance OrderDual.instVAddCommClass'' {M : Type u_1} {N : Type u_2} {α : Type u_3} [VAdd M α] [VAdd N α] [VAddCommClass M N α] :
VAddCommClass M N αᵒᵈ
Equations
  • ⋯ = inst
source
instance OrderDual.instSMulCommClass'' {M : Type u_1} {N : Type u_2} {α : Type u_3} [SMul M α] [SMul N α] [SMulCommClass M N α] :
SMulCommClass M N αᵒᵈ
Equations
  • ⋯ = inst
source
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 α
Equations
  • ⋯ = inst
source
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 α
Equations
  • ⋯ = inst
source
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ᵒᵈ α
Equations
  • ⋯ = inst
source
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ᵒᵈ α
Equations
  • ⋯ = inst
source
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 αᵒᵈ
Equations
  • ⋯ = inst
source
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 αᵒᵈ
Equations
  • ⋯ = inst
source
instance Lex.instAddAction {M : Type u_1} {α : Type u_3} [AddMonoid M] [AddAction M α] :
AddAction (Lex M) α
Equations
  • Lex.instAddAction = inst
source
instance Lex.instMulAction {M : Type u_1} {α : Type u_3} [Monoid M] [MulAction M α] :
MulAction (Lex M) α
Equations
  • Lex.instMulAction = inst
source
instance Lex.instAddAction' {M : Type u_1} {α : Type u_3} [AddMonoid M] [AddAction M α] :
AddAction M (Lex α)
Equations
  • Lex.instAddAction' = inst
source
instance Lex.instMulAction' {M : Type u_1} {α : Type u_3} [Monoid M] [MulAction M α] :
MulAction M (Lex α)
Equations
  • Lex.instMulAction' = inst
source
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 α
Equations
  • ⋯ = inst
source
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 α
Equations
  • ⋯ = inst
source
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) α
Equations
  • ⋯ = inst
source
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) α
Equations
  • ⋯ = inst
source
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 α)
Equations
  • ⋯ = inst
source
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 α)
Equations
  • ⋯ = inst
source
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 α
Equations
  • ⋯ = inst
source
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 α
Equations
  • ⋯ = inst
source
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) α
Equations
  • ⋯ = inst
source
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) α
Equations
  • ⋯ = inst
source
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 α)
Equations
  • ⋯ = inst
source
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 α)
Equations
  • ⋯ = inst