Ring structure on the order type synonyms #
Transfer algebraic instances from α
to αᵒᵈ
and lex α
.
Order dual #
instance
instLeftDistribClassOrderDualInstMulOrderDualInstAddOrderDual
{α : Type u_1}
[inst : Mul α]
[inst : Add α]
[h : LeftDistribClass α]
:
Equations
- instLeftDistribClassOrderDualInstMulOrderDualInstAddOrderDual = h
instance
instRightDistribClassOrderDualInstMulOrderDualInstAddOrderDual
{α : Type u_1}
[inst : Mul α]
[inst : Add α]
[h : RightDistribClass α]
:
Equations
- instRightDistribClassOrderDualInstMulOrderDualInstAddOrderDual = h
Equations
- instNonUnitalNonAssocSemiringOrderDual = h
Equations
- instNonUnitalSemiringOrderDual = h
Equations
- instNonAssocSemiringOrderDual = h
Equations
- instNonUnitalCommSemiringOrderDual = h
Equations
- instCommSemiringOrderDual = h
instance
instHasDistribNegOrderDualInstMulOrderDual
{α : Type u_1}
[inst : Mul α]
[h : HasDistribNeg α]
:
Equations
- instHasDistribNegOrderDualInstMulOrderDual = h
Equations
- instNonUnitalNonAssocRingOrderDual = h
Equations
- instNonUnitalRingOrderDual = h
Equations
- instNonAssocRingOrderDual = h
Equations
- instNonUnitalCommRingOrderDual = h
instance
instIsDomainOrderDualInstSemiringOrderDualToSemiring
{α : Type u_1}
[inst : Ring α]
[h : IsDomain α]
:
Lexicographical order #
instance
instLeftDistribClassLexInstMulLexInstAddLex
{α : Type u_1}
[inst : Mul α]
[inst : Add α]
[h : LeftDistribClass α]
:
LeftDistribClass (Lex α)
Equations
- instLeftDistribClassLexInstMulLexInstAddLex = h
instance
instRightDistribClassLexInstMulLexInstAddLex
{α : Type u_1}
[inst : Mul α]
[inst : Add α]
[h : RightDistribClass α]
:
RightDistribClass (Lex α)
Equations
- instRightDistribClassLexInstMulLexInstAddLex = h
Equations
- instNonUnitalNonAssocSemiringLex = h
instance
instNonUnitalSemiringLex
{α : Type u_1}
[h : NonUnitalSemiring α]
:
NonUnitalSemiring (Lex α)
Equations
- instNonUnitalSemiringLex = h
Equations
- instNonAssocSemiringLex = h
Equations
- instNonUnitalCommSemiringLex = h
Equations
- instCommSemiringLex = h
instance
instHasDistribNegLexInstMulLex
{α : Type u_1}
[inst : Mul α]
[h : HasDistribNeg α]
:
HasDistribNeg (Lex α)
Equations
- instHasDistribNegLexInstMulLex = h
Equations
- instNonUnitalNonAssocRingLex = h
Equations
- instNonUnitalRingLex = h
Equations
- instNonAssocRingLex = h
instance
instNonUnitalCommRingLex
{α : Type u_1}
[h : NonUnitalCommRing α]
:
NonUnitalCommRing (Lex α)
Equations
- instNonUnitalCommRingLex = h