Documentation

Mathlib.Algebra.Order.Ring.Synonym

Ring structure on the order type synonyms #

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

Order dual #

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 instNonUnitalNonAssocSemiringOrderDual {R : Type u_1} [h : NonUnitalNonAssocSemiring R] :

NonUnitalNonAssocSemiring Rᵒᵈ

Equations

instNonUnitalNonAssocSemiringOrderDual = h

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

NonUnitalSemiring Rᵒᵈ

Equations

instNonUnitalSemiringOrderDual = h

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

NonAssocSemiring Rᵒᵈ

Equations

instNonAssocSemiringOrderDual = h

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

Semiring Rᵒᵈ

Equations

instSemiringOrderDual = h

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

NonUnitalCommSemiring Rᵒᵈ

Equations

instNonUnitalCommSemiringOrderDual = h

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

CommSemiring Rᵒᵈ

Equations

instCommSemiringOrderDual = h

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

HasDistribNeg Rᵒᵈ

Equations

instHasDistribNegOrderDual = h

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

NonUnitalNonAssocRing Rᵒᵈ

Equations

instNonUnitalNonAssocRingOrderDual = h

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

NonUnitalRing Rᵒᵈ

Equations

instNonUnitalRingOrderDual = h

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

NonAssocRing Rᵒᵈ

Equations

instNonAssocRingOrderDual = h

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

Equations

instRingOrderDual = h

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

NonUnitalCommRing Rᵒᵈ

Equations

instNonUnitalCommRingOrderDual = h

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 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 instNonUnitalNonAssocSemiringLex {R : Type u_1} [h : NonUnitalNonAssocSemiring R] :

NonUnitalNonAssocSemiring (Lex R)

Equations

instNonUnitalNonAssocSemiringLex = h

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

NonUnitalSemiring (Lex R)

Equations

instNonUnitalSemiringLex = h

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

NonAssocSemiring (Lex R)

Equations

instNonAssocSemiringLex = h

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

Semiring (Lex R)

Equations

instSemiringLex = h

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

NonUnitalCommSemiring (Lex R)

Equations

instNonUnitalCommSemiringLex = h

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

CommSemiring (Lex R)

Equations

instCommSemiringLex = h

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

HasDistribNeg (Lex R)

Equations

instHasDistribNegLex = h

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

NonUnitalNonAssocRing (Lex R)

Equations

instNonUnitalNonAssocRingLex = h

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

NonUnitalRing (Lex R)

Equations

instNonUnitalRingLex = h

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

NonAssocRing (Lex R)

Equations

instNonAssocRingLex = h

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

Equations

instRingLex = h

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

NonUnitalCommRing (Lex R)

Equations

instNonUnitalCommRingLex = h

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)