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.

See also

• Mathlib.Algebra.Order.Group.Action.Synonym
• Mathlib.Algebra.Order.GroupWithZero.Action.Synonym

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

Equations

• OrderDual.instModule = Module.mk ⋯ ⋯

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

Equations

• OrderDual.instModule' = Module.mk ⋯ ⋯

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

Equations

• Lex.instModule = inst

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

Equations

• Lex.instModule' = inst