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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• OrderDual.instModule' = { toDistribMulAction := OrderDual.instDistribMulAction_1, add_smul := ⋯, zero_smul := ⋯ }

@[instance_reducible]

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

Equations

• Lex.instModule = inst✝

@[instance_reducible]

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

Equations

• Lex.instModule' = inst✝