Ring structure on the order type synonyms

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

Order dual

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

Equations

• instDistribOrderDual = h

instance instLeftDistribClassOrderDualInstMulOrderDualInstAddOrderDual {α : Type u_1} [Mul α] [Add α] [h : LeftDistribClass α] : LeftDistribClass αᵒᵈ

Equations

• (_ : LeftDistribClass αᵒᵈ) = h

instance instRightDistribClassOrderDualInstMulOrderDualInstAddOrderDual {α : Type u_1} [Mul α] [Add α] [h : RightDistribClass α] : RightDistribClass αᵒᵈ

Equations

• (_ : RightDistribClass αᵒᵈ) = h

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

Equations

• instNonUnitalNonAssocSemiringOrderDual = h

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

Equations

• instNonUnitalSemiringOrderDual = h

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

Equations

• instNonAssocSemiringOrderDual = h

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

Equations

• instSemiringOrderDual = h

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

Equations

• instNonUnitalCommSemiringOrderDual = h

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

Equations

• instCommSemiringOrderDual = h

instance instHasDistribNegOrderDualInstMulOrderDual {α : Type u_1} [Mul α] [h : HasDistribNeg α] : HasDistribNeg αᵒᵈ

Equations

• instHasDistribNegOrderDualInstMulOrderDual = h

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

Equations

• instNonUnitalNonAssocRingOrderDual = h

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

Equations

• instNonUnitalRingOrderDual = h

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

Equations

• instNonAssocRingOrderDual = h

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

Equations

• instRingOrderDual = h

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

Equations

• instNonUnitalCommRingOrderDual = h

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

Equations

• instCommRingOrderDual = h

instance instIsDomainOrderDualInstSemiringOrderDualToSemiring {α : Type u_1} [Ring α] [h : IsDomain α] : IsDomain αᵒᵈ

Equations

• (_ : IsDomain αᵒᵈ) = h

Lexicographical order

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

Equations

• instDistribLex = h

instance instLeftDistribClassLexInstMulLexInstAddLex {α : Type u_1} [Mul α] [Add α] [h : LeftDistribClass α] : LeftDistribClass (Lex α)

Equations

• (_ : LeftDistribClass (Lex α)) = h

instance instRightDistribClassLexInstMulLexInstAddLex {α : Type u_1} [Mul α] [Add α] [h : RightDistribClass α] : RightDistribClass (Lex α)

Equations

• (_ : RightDistribClass (Lex α)) = h

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

Equations

• instNonUnitalNonAssocSemiringLex = h

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

Equations

• instNonUnitalSemiringLex = h

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

Equations

• instNonAssocSemiringLex = h

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

Equations

• instSemiringLex = h

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

Equations

• instNonUnitalCommSemiringLex = h

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

Equations

• instCommSemiringLex = h

instance instHasDistribNegLexInstMulLex {α : Type u_1} [Mul α] [h : HasDistribNeg α] : HasDistribNeg (Lex α)

Equations

• instHasDistribNegLexInstMulLex = h

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

Equations

• instNonUnitalNonAssocRingLex = h

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

Equations

• instNonUnitalRingLex = h

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

Equations

• instNonAssocRingLex = h

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

Equations

• instRingLex = h

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

Equations

• instNonUnitalCommRingLex = h

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

Equations

• instCommRingLex = h

instance instIsDomainLexInstSemiringLexToSemiring {α : Type u_1} [Ring α] [h : IsDomain α] : IsDomain (Lex α)

Equations

• (_ : IsDomain (Lex α)) = h