# Actions by and on order synonyms #

This PR transfers group action with zero instances from a type `α` to `αᵒᵈ` and `Lex α`. Note that the `SMul` instances are already defined in `Mathlib/Algebra/Order/Group/Synonym.lean`.

## See also #

- `Mathlib/Algebra/Order/Group/Action/Synonym.lean`
- `Mathlib/Algebra/Order/Module/Synonym.lean`

source
instance OrderDual.instSMulWithZero {G₀ : Type u_1} {M₀ : Type u_2} [Zero G₀] [Zero M₀] [SMulWithZero G₀ M₀] :
SMulWithZero G₀ ᵒᵈ M₀
Equations

- OrderDual.instSMulWithZero = inst✝

source
instance OrderDual.instSMulWithZero' {G₀ : Type u_1} {M₀ : Type u_2} [Zero G₀] [Zero M₀] [SMulWithZero G₀ M₀] :
SMulWithZero G₀ M₀ ᵒᵈ
Equations

- OrderDual.instSMulWithZero' = inst✝

source
instance OrderDual.instDistribSMul {G₀ : Type u_1} {M₀ : Type u_2} [AddZeroClass M₀] [DistribSMul G₀ M₀] :
DistribSMul G₀ ᵒᵈ M₀
Equations

- OrderDual.instDistribSMul = inst✝

source
instance OrderDual.instDistribSMul' {G₀ : Type u_1} {M₀ : Type u_2} [AddZeroClass M₀] [DistribSMul G₀ M₀] :
DistribSMul G₀ M₀ ᵒᵈ
Equations

- OrderDual.instDistribSMul' = inst✝

source
instance OrderDual.instDistribMulAction {G₀ : Type u_1} {M₀ : Type u_2} [Monoid G₀] [AddMonoid M₀] [DistribMulAction G₀ M₀] :
DistribMulAction G₀ ᵒᵈ M₀
Equations

- OrderDual.instDistribMulAction = inst✝

source
instance OrderDual.instDistribMulAction' {G₀ : Type u_1} {M₀ : Type u_2} [Monoid G₀] [AddMonoid M₀] [DistribMulAction G₀ M₀] :
DistribMulAction G₀ M₀ ᵒᵈ
Equations

- OrderDual.instDistribMulAction' = inst✝

source
instance OrderDual.instMulActionWithZero {G₀ : Type u_1} {M₀ : Type u_2} [MonoidWithZero G₀] [AddMonoid M₀] [MulActionWithZero G₀ M₀] :
MulActionWithZero G₀ ᵒᵈ M₀
Equations

- OrderDual.instMulActionWithZero = inst✝

source
instance OrderDual.instMulActionWithZero' {G₀ : Type u_1} {M₀ : Type u_2} [MonoidWithZero G₀] [AddMonoid M₀] [MulActionWithZero G₀ M₀] :
MulActionWithZero G₀ M₀ ᵒᵈ
Equations

- OrderDual.instMulActionWithZero' = inst✝

source
instance Lex.instSMulWithZero {G₀ : Type u_1} {M₀ : Type u_2} [Zero G₀] [Zero M₀] [SMulWithZero G₀ M₀] :
SMulWithZero (Lex G₀) M₀
Equations

- Lex.instSMulWithZero = inst✝

source
instance Lex.instSMulWithZero' {G₀ : Type u_1} {M₀ : Type u_2} [Zero G₀] [Zero M₀] [SMulWithZero G₀ M₀] :
SMulWithZero G₀ (Lex M₀)
Equations

- Lex.instSMulWithZero' = inst✝

source
instance Lex.instDistribSMul {G₀ : Type u_1} {M₀ : Type u_2} [AddZeroClass M₀] [DistribSMul G₀ M₀] :
DistribSMul (Lex G₀) M₀
Equations

- Lex.instDistribSMul = inst✝

source
instance Lex.instDistribSMul' {G₀ : Type u_1} {M₀ : Type u_2} [AddZeroClass M₀] [DistribSMul G₀ M₀] :
DistribSMul G₀ (Lex M₀)
Equations

- Lex.instDistribSMul' = inst✝

source
instance Lex.instDistribMulAction {G₀ : Type u_1} {M₀ : Type u_2} [Monoid G₀] [AddMonoid M₀] [DistribMulAction G₀ M₀] :
DistribMulAction (Lex G₀) M₀
Equations

- Lex.instDistribMulAction = inst✝

source
instance Lex.instDistribMulAction' {G₀ : Type u_1} {M₀ : Type u_2} [Monoid G₀] [AddMonoid M₀] [DistribMulAction G₀ M₀] :
DistribMulAction G₀ (Lex M₀)
Equations

- Lex.instDistribMulAction' = inst✝

source
instance Lex.instMulActionWithZero {G₀ : Type u_1} {M₀ : Type u_2} [MonoidWithZero G₀] [AddMonoid M₀] [MulActionWithZero G₀ M₀] :
MulActionWithZero (Lex G₀) M₀
Equations

- Lex.instMulActionWithZero = inst✝

source
instance Lex.instMulActionWithZero' {G₀ : Type u_1} {M₀ : Type u_2} [MonoidWithZero G₀] [AddMonoid M₀] [MulActionWithZero G₀ M₀] :
MulActionWithZero G₀ (Lex M₀)
Equations

- Lex.instMulActionWithZero' = inst✝