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 #

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

Module αᵒᵈ β

Equations

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

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

Module α βᵒᵈ

Equations

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

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✝