Ring structure on the order type synonyms

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

Order dual

ink

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

Equations

• instDistribOrderDual = h

ink

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

Equations

• instLeftDistribClassOrderDualInstMulOrderDualInstAddOrderDual = h

ink

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

Equations

• instRightDistribClassOrderDualInstMulOrderDualInstAddOrderDual = h

ink

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

Equations

• instNonUnitalNonAssocSemiringOrderDual = h

ink

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

Equations

• instNonUnitalSemiringOrderDual = h

ink

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

Equations

• instNonAssocSemiringOrderDual = h

ink

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

Equations

• instSemiringOrderDual = h

ink

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

Equations

• instNonUnitalCommSemiringOrderDual = h

ink

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

Equations

• instCommSemiringOrderDual = h

ink

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

Equations

• instHasDistribNegOrderDualInstMulOrderDual = h

ink

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

Equations

• instNonUnitalNonAssocRingOrderDual = h

ink

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

Equations

• instNonUnitalRingOrderDual = h

ink

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

Equations

• instNonAssocRingOrderDual = h

ink

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

Equations

• instRingOrderDual = h

ink

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

Equations

• instNonUnitalCommRingOrderDual = h

ink

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

Equations

• instCommRingOrderDual = h

ink

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

Equations

• @instIsDomainOrderDualInstSemiringOrderDualToSemiring = @instIsDomainOrderDualInstSemiringOrderDualToSemiring.proof_1

Lexicographical order

ink

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

Equations

• instDistribLex = h

ink

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

Equations

• instLeftDistribClassLexInstMulLexInstAddLex = h

ink

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

Equations

• instRightDistribClassLexInstMulLexInstAddLex = h

ink

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

Equations

• instNonUnitalNonAssocSemiringLex = h

ink

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

Equations

• instNonUnitalSemiringLex = h

ink

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

Equations

• instNonAssocSemiringLex = h

ink

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

Equations

• instSemiringLex = h

ink

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

Equations

• instNonUnitalCommSemiringLex = h

ink

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

Equations

• instCommSemiringLex = h

ink

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

Equations

• instHasDistribNegLexInstMulLex = h

ink

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

Equations

• instNonUnitalNonAssocRingLex = h

ink

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

Equations

• instNonUnitalRingLex = h

ink

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

Equations

• instNonAssocRingLex = h

ink

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

Equations

• instRingLex = h

ink

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

Equations

• instNonUnitalCommRingLex = h

ink

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

Equations

• instCommRingLex = h

ink

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

Equations

• @instIsDomainLexInstSemiringLexToSemiring = @instIsDomainLexInstSemiringLexToSemiring.proof_1