Ring structure on the order type synonyms

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

Order dual

@[instance_reducible]

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

Equations

• instDistribOrderDual = h

instance instLeftDistribClassOrderDual {R : Type u_1} [Mul R] [Add R] [h : LeftDistribClass R] : LeftDistribClass Rᵒᵈ

instance instRightDistribClassOrderDual {R : Type u_1} [Mul R] [Add R] [h : RightDistribClass R] : RightDistribClass Rᵒᵈ

@[instance_reducible]

instance instNonUnitalNonAssocSemiringOrderDual {R : Type u_1} [h : NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring Rᵒᵈ

Equations

• instNonUnitalNonAssocSemiringOrderDual = h

@[instance_reducible]

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

Equations

• instNonUnitalSemiringOrderDual = h

@[instance_reducible]

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

Equations

• instNonAssocSemiringOrderDual = h

@[instance_reducible]

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

Equations

• instSemiringOrderDual = h

@[instance_reducible]

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

Equations

• instNonUnitalCommSemiringOrderDual = h

@[instance_reducible]

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

Equations

• instCommSemiringOrderDual = h

@[instance_reducible]

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

Equations

• instHasDistribNegOrderDual = h

@[instance_reducible]

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

Equations

• instNonUnitalNonAssocRingOrderDual = h

@[instance_reducible]

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

Equations

• instNonUnitalRingOrderDual = h

@[instance_reducible]

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

Equations

• instNonAssocRingOrderDual = h

@[instance_reducible]

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

Equations

• instRingOrderDual = h

@[instance_reducible]

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

Equations

• instNonUnitalCommRingOrderDual = h

@[instance_reducible]

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

Equations

• instCommRingOrderDual = h

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

Lexicographical order

@[instance_reducible]

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

Equations

• instDistribLex = h

instance instLeftDistribClassLex {R : Type u_1} [Mul R] [Add R] [h : LeftDistribClass R] : LeftDistribClass (Lex R)

instance instRightDistribClassLex {R : Type u_1} [Mul R] [Add R] [h : RightDistribClass R] : RightDistribClass (Lex R)

@[instance_reducible]

instance instNonUnitalNonAssocSemiringLex {R : Type u_1} [h : NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring (Lex R)

Equations

• instNonUnitalNonAssocSemiringLex = h

@[instance_reducible]

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

Equations

• instNonUnitalSemiringLex = h

@[instance_reducible]

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

Equations

• instNonAssocSemiringLex = h

@[instance_reducible]

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

Equations

• instSemiringLex = h

@[instance_reducible]

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

Equations

• instNonUnitalCommSemiringLex = h

@[instance_reducible]

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

Equations

• instCommSemiringLex = h

@[instance_reducible]

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

Equations

• instHasDistribNegLex = h

@[instance_reducible]

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

Equations

• instNonUnitalNonAssocRingLex = h

@[instance_reducible]

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

Equations

• instNonUnitalRingLex = h

@[instance_reducible]

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

Equations

• instNonAssocRingLex = h

@[instance_reducible]

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

Equations

• instRingLex = h

@[instance_reducible]

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

Equations

• instNonUnitalCommRingLex = h

@[instance_reducible]

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

Equations

• instCommRingLex = h

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