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 OrderDual.instModule {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] :
Module αᵒᵈ β
Equations
    source
    instance OrderDual.instModule' {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] :
    Module α βᵒᵈ
    Equations
      source
      instance Lex.instModule {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] :
      Module (Lex α) β
      Equations
        source
        instance Lex.instModule' {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] :
        Module α (Lex β)
        Equations