Documentation

Mathlib.Algebra.Ring.OrderSynonym

Ring structure on the order type synonyms #

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

Order dual #

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

Distrib αᵒᵈ

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

LeftDistribClass αᵒᵈ

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

RightDistribClass αᵒᵈ

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

NonUnitalNonAssocSemiring αᵒᵈ

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

NonUnitalSemiring αᵒᵈ

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

NonAssocSemiring αᵒᵈ

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

Semiring αᵒᵈ

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

NonUnitalCommSemiring αᵒᵈ

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

CommSemiring αᵒᵈ

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

HasDistribNeg αᵒᵈ

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

NonUnitalNonAssocRing αᵒᵈ

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

NonUnitalRing αᵒᵈ

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

NonAssocRing αᵒᵈ

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

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

NonUnitalCommRing αᵒᵈ

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

CommRing αᵒᵈ

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

IsDomain αᵒᵈ

Lexicographical order #

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

Distrib (Lex α)

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

LeftDistribClass (Lex α)

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

RightDistribClass (Lex α)

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

NonUnitalNonAssocSemiring (Lex α)

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

NonUnitalSemiring (Lex α)

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

NonAssocSemiring (Lex α)

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

Semiring (Lex α)

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

NonUnitalCommSemiring (Lex α)

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

CommSemiring (Lex α)

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

HasDistribNeg (Lex α)

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

NonUnitalNonAssocRing (Lex α)

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

NonUnitalRing (Lex α)

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

NonAssocRing (Lex α)

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

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

NonUnitalCommRing (Lex α)

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

CommRing (Lex α)

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

IsDomain (Lex α)