# Documentation

Mathlib.Algebra.Ring.OrderSynonym

# Ring structure on the order type synonyms #

Transfer algebraic instances from α to αᵒᵈ and lex α.

### Order dual #

instance instDistribOrderDual {α : Type u_1} [h : ] :
Equations
• instDistribOrderDual = h
instance instLeftDistribClassOrderDualInstMulOrderDualInstAddOrderDual {α : Type u_1} [inst : Mul α] [inst : Add α] [h : ] :
Equations
instance instRightDistribClassOrderDualInstMulOrderDualInstAddOrderDual {α : Type u_1} [inst : Mul α] [inst : Add α] [h : ] :
Equations
instance instNonUnitalNonAssocSemiringOrderDual {α : Type u_1} [h : ] :
Equations
• instNonUnitalNonAssocSemiringOrderDual = h
instance instNonUnitalSemiringOrderDual {α : Type u_1} [h : ] :
Equations
• instNonUnitalSemiringOrderDual = h
instance instNonAssocSemiringOrderDual {α : Type u_1} [h : ] :
Equations
• instNonAssocSemiringOrderDual = h
instance instSemiringOrderDual {α : Type u_1} [h : ] :
Equations
• instSemiringOrderDual = h
instance instNonUnitalCommSemiringOrderDual {α : Type u_1} [h : ] :
Equations
• instNonUnitalCommSemiringOrderDual = h
instance instCommSemiringOrderDual {α : Type u_1} [h : ] :
Equations
• instCommSemiringOrderDual = h
instance instHasDistribNegOrderDualInstMulOrderDual {α : Type u_1} [inst : Mul α] [h : ] :
Equations
• instHasDistribNegOrderDualInstMulOrderDual = h
instance instNonUnitalNonAssocRingOrderDual {α : Type u_1} [h : ] :
Equations
• instNonUnitalNonAssocRingOrderDual = h
instance instNonUnitalRingOrderDual {α : Type u_1} [h : ] :
Equations
• instNonUnitalRingOrderDual = h
instance instNonAssocRingOrderDual {α : Type u_1} [h : ] :
Equations
• instNonAssocRingOrderDual = h
instance instRingOrderDual {α : Type u_1} [h : Ring α] :
Equations
• instRingOrderDual = h
instance instNonUnitalCommRingOrderDual {α : Type u_1} [h : ] :
Equations
• instNonUnitalCommRingOrderDual = h
instance instCommRingOrderDual {α : Type u_1} [h : ] :
Equations
• instCommRingOrderDual = h
instance instIsDomainOrderDualInstSemiringOrderDualToSemiring {α : Type u_1} [inst : Ring α] [h : ] :
Equations

### Lexicographical order #

instance instDistribLex {α : Type u_1} [h : ] :
Equations
• instDistribLex = h
instance instLeftDistribClassLexInstMulLexInstAddLex {α : Type u_1} [inst : Mul α] [inst : Add α] [h : ] :
Equations
instance instRightDistribClassLexInstMulLexInstAddLex {α : Type u_1} [inst : Mul α] [inst : Add α] [h : ] :
Equations
instance instNonUnitalNonAssocSemiringLex {α : Type u_1} [h : ] :
Equations
• instNonUnitalNonAssocSemiringLex = h
instance instNonUnitalSemiringLex {α : Type u_1} [h : ] :
Equations
• instNonUnitalSemiringLex = h
instance instNonAssocSemiringLex {α : Type u_1} [h : ] :
Equations
• instNonAssocSemiringLex = h
instance instSemiringLex {α : Type u_1} [h : ] :
Equations
• instSemiringLex = h
instance instNonUnitalCommSemiringLex {α : Type u_1} [h : ] :
Equations
• instNonUnitalCommSemiringLex = h
instance instCommSemiringLex {α : Type u_1} [h : ] :
Equations
• instCommSemiringLex = h
instance instHasDistribNegLexInstMulLex {α : Type u_1} [inst : Mul α] [h : ] :
Equations
• instHasDistribNegLexInstMulLex = h
instance instNonUnitalNonAssocRingLex {α : Type u_1} [h : ] :
Equations
• instNonUnitalNonAssocRingLex = h
instance instNonUnitalRingLex {α : Type u_1} [h : ] :
Equations
• instNonUnitalRingLex = h
instance instNonAssocRingLex {α : Type u_1} [h : ] :
Equations
• instNonAssocRingLex = h
instance instRingLex {α : Type u_1} [h : Ring α] :
Ring (Lex α)
Equations
• instRingLex = h
instance instNonUnitalCommRingLex {α : Type u_1} [h : ] :
Equations
• instNonUnitalCommRingLex = h
instance instCommRingLex {α : Type u_1} [h : ] :
Equations
• instCommRingLex = h
instance instIsDomainLexInstSemiringLexToSemiring {α : Type u_1} [inst : Ring α] [h : ] :
Equations