Documentation

Mathlib.Algebra.Order.Module.Synonym

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 #

source
@[instance_reducible]
instance OrderDual.instModule {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] :
Module αᵒᵈ β
source
@[instance_reducible]
instance OrderDual.instModule' {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] :
Module α βᵒᵈ
source
@[instance_reducible]
instance Lex.instModule {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] :
Module (Lex α) β
source
@[instance_reducible]
instance Lex.instModule' {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] :
Module α (Lex β)