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

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

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

NonUnitalSemiring Rᵒᵈ

Equations

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

NonAssocSemiring Rᵒᵈ

Equations

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

Semiring Rᵒᵈ

Equations

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

NonUnitalCommSemiring Rᵒᵈ

Equations

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

CommSemiring Rᵒᵈ

Equations

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

HasDistribNeg Rᵒᵈ

Equations

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

NonUnitalNonAssocRing Rᵒᵈ

Equations

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

NonUnitalRing Rᵒᵈ

Equations

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

NonAssocRing Rᵒᵈ

Equations

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

Equations

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

NonUnitalCommRing Rᵒᵈ

Equations

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

CommRing Rᵒᵈ

Equations

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

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

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

NonUnitalSemiring (Lex R)

Equations

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

NonAssocSemiring (Lex R)

Equations

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

Semiring (Lex R)

Equations

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

NonUnitalCommSemiring (Lex R)

Equations

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

CommSemiring (Lex R)

Equations

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

HasDistribNeg (Lex R)

Equations

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

NonUnitalNonAssocRing (Lex R)

Equations

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

NonUnitalRing (Lex R)

Equations

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

NonAssocRing (Lex R)

Equations

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

Equations

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

NonUnitalCommRing (Lex R)

Equations

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

CommRing (Lex R)

Equations

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

IsDomain (Lex R)