Order dual #
instance
instLeftDistribClassOrderDualInstMulOrderDualInstAddOrderDual
{α : Type u_1}
[Mul α]
[Add α]
[h : LeftDistribClass α]
:
instance
instRightDistribClassOrderDualInstMulOrderDualInstAddOrderDual
{α : Type u_1}
[Mul α]
[Add α]
[h : RightDistribClass α]
:
Lexicographical order #
instance
instLeftDistribClassLexInstMulLexInstAddLex
{α : Type u_1}
[Mul α]
[Add α]
[h : LeftDistribClass α]
:
LeftDistribClass (Lex α)
instance
instRightDistribClassLexInstMulLexInstAddLex
{α : Type u_1}
[Mul α]
[Add α]
[h : RightDistribClass α]
:
RightDistribClass (Lex α)
instance
instNonUnitalSemiringLex
{α : Type u_1}
[h : NonUnitalSemiring α]
:
NonUnitalSemiring (Lex α)
instance
instHasDistribNegLexInstMulLex
{α : Type u_1}
[Mul α]
[h : HasDistribNeg α]
:
HasDistribNeg (Lex α)
instance
instNonUnitalCommRingLex
{α : Type u_1}
[h : NonUnitalCommRing α]
:
NonUnitalCommRing (Lex α)