# Action instances for `OrderDual` #

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/GroupWithZero/Action/Synonym.lean`

source
instance OrderDual.instModule {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] :
Module α ᵒᵈ β
Equations

- OrderDual.instModule = { toDistribMulAction := OrderDual.instDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

source
instance OrderDual.instModule' {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] :
Module α β ᵒᵈ
Equations

- OrderDual.instModule' = { toDistribMulAction := OrderDual.instDistribMulAction', add_smul := ⋯, zero_smul := ⋯ }

source
instance Lex.instModule {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] :
Module (Lex α) β
Equations

- Lex.instModule = inst✝

source
instance Lex.instModule' {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] :
Module α (Lex β)
Equations

- Lex.instModule' = inst✝