# Ring structure on the order type synonyms #

Transfer algebraic instances from `R` to `Rᵒᵈ` and `Lex R`.

### Order dual #

source
instance instDistribOrderDual {R : Type u_1} [h : Distrib R] :
Distrib R ᵒᵈ
Equations

- instDistribOrderDual = h

source
instance instLeftDistribClassOrderDual {R : Type u_1} [Mul R] [Add R] [h : LeftDistribClass R] :
LeftDistribClass R ᵒᵈ
source
instance instRightDistribClassOrderDual {R : Type u_1} [Mul R] [Add R] [h : RightDistribClass R] :
RightDistribClass R ᵒᵈ
source
instance instNonUnitalNonAssocSemiringOrderDual {R : Type u_1} [h : NonUnitalNonAssocSemiring R] :
NonUnitalNonAssocSemiring R ᵒᵈ
Equations

- instNonUnitalNonAssocSemiringOrderDual = h

source
instance instNonUnitalSemiringOrderDual {R : Type u_1} [h : NonUnitalSemiring R] :
NonUnitalSemiring R ᵒᵈ
Equations

- instNonUnitalSemiringOrderDual = h

source
instance instNonAssocSemiringOrderDual {R : Type u_1} [h : NonAssocSemiring R] :
NonAssocSemiring R ᵒᵈ
Equations

- instNonAssocSemiringOrderDual = h

source
instance instSemiringOrderDual {R : Type u_1} [h : Semiring R] :
Semiring R ᵒᵈ
Equations

- instSemiringOrderDual = h

source
instance instNonUnitalCommSemiringOrderDual {R : Type u_1} [h : NonUnitalCommSemiring R] :
NonUnitalCommSemiring R ᵒᵈ
Equations

- instNonUnitalCommSemiringOrderDual = h

source
instance instCommSemiringOrderDual {R : Type u_1} [h : CommSemiring R] :
CommSemiring R ᵒᵈ
Equations

- instCommSemiringOrderDual = h

source
instance instHasDistribNegOrderDual {R : Type u_1} [Mul R] [h : HasDistribNeg R] :
HasDistribNeg R ᵒᵈ
Equations

- instHasDistribNegOrderDual = h

source
instance instNonUnitalNonAssocRingOrderDual {R : Type u_1} [h : NonUnitalNonAssocRing R] :
NonUnitalNonAssocRing R ᵒᵈ
Equations

- instNonUnitalNonAssocRingOrderDual = h

source
instance instNonUnitalRingOrderDual {R : Type u_1} [h : NonUnitalRing R] :
NonUnitalRing R ᵒᵈ
Equations

- instNonUnitalRingOrderDual = h

source
instance instNonAssocRingOrderDual {R : Type u_1} [h : NonAssocRing R] :
NonAssocRing R ᵒᵈ
Equations

- instNonAssocRingOrderDual = h

source
instance instRingOrderDual {R : Type u_1} [h : Ring R] :
Ring R ᵒᵈ
Equations

- instRingOrderDual = h

source
instance instNonUnitalCommRingOrderDual {R : Type u_1} [h : NonUnitalCommRing R] :
NonUnitalCommRing R ᵒᵈ
Equations

- instNonUnitalCommRingOrderDual = h

source
instance instCommRingOrderDual {R : Type u_1} [h : CommRing R] :
CommRing R ᵒᵈ
Equations

- instCommRingOrderDual = h

source
instance instIsDomainOrderDual {R : Type u_1} [Ring R] [h : IsDomain R] :
IsDomain R ᵒᵈ

### Lexicographical order #

source
instance instDistribLex {R : Type u_1} [h : Distrib R] :
Distrib (Lex R)
Equations

- instDistribLex = h

source
instance instLeftDistribClassLex {R : Type u_1} [Mul R] [Add R] [h : LeftDistribClass R] :
LeftDistribClass (Lex R)
source
instance instRightDistribClassLex {R : Type u_1} [Mul R] [Add R] [h : RightDistribClass R] :
RightDistribClass (Lex R)
source
instance instNonUnitalNonAssocSemiringLex {R : Type u_1} [h : NonUnitalNonAssocSemiring R] :
NonUnitalNonAssocSemiring (Lex R)
Equations

- instNonUnitalNonAssocSemiringLex = h

source
instance instNonUnitalSemiringLex {R : Type u_1} [h : NonUnitalSemiring R] :
NonUnitalSemiring (Lex R)
Equations

- instNonUnitalSemiringLex = h

source
instance instNonAssocSemiringLex {R : Type u_1} [h : NonAssocSemiring R] :
NonAssocSemiring (Lex R)
Equations

- instNonAssocSemiringLex = h

source
instance instSemiringLex {R : Type u_1} [h : Semiring R] :
Semiring (Lex R)
Equations

- instSemiringLex = h

source
instance instNonUnitalCommSemiringLex {R : Type u_1} [h : NonUnitalCommSemiring R] :
NonUnitalCommSemiring (Lex R)
Equations

- instNonUnitalCommSemiringLex = h

source
instance instCommSemiringLex {R : Type u_1} [h : CommSemiring R] :
CommSemiring (Lex R)
Equations

- instCommSemiringLex = h

source
instance instHasDistribNegLex {R : Type u_1} [Mul R] [h : HasDistribNeg R] :
HasDistribNeg (Lex R)
Equations

- instHasDistribNegLex = h

source
instance instNonUnitalNonAssocRingLex {R : Type u_1} [h : NonUnitalNonAssocRing R] :
NonUnitalNonAssocRing (Lex R)
Equations

- instNonUnitalNonAssocRingLex = h

source
instance instNonUnitalRingLex {R : Type u_1} [h : NonUnitalRing R] :
NonUnitalRing (Lex R)
Equations

- instNonUnitalRingLex = h

source
instance instNonAssocRingLex {R : Type u_1} [h : NonAssocRing R] :
NonAssocRing (Lex R)
Equations

- instNonAssocRingLex = h

source
instance instRingLex {R : Type u_1} [h : Ring R] :
Ring (Lex R)
Equations

- instRingLex = h

source
instance instNonUnitalCommRingLex {R : Type u_1} [h : NonUnitalCommRing R] :
NonUnitalCommRing (Lex R)
Equations

- instNonUnitalCommRingLex = h

source
instance instCommRingLex {R : Type u_1} [h : CommRing R] :
CommRing (Lex R)
Equations

- instCommRingLex = h

source
instance instIsDomainLex {R : Type u_1} [Ring R] [h : IsDomain R] :
IsDomain (Lex R)