HepLean Documentation

Mathlib.Algebra.Order.Ring.Synonym

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 instLeftDistribClassOrderDual {α : Type u_1} [Mul α] [Add α] [h : LeftDistribClass α] :

LeftDistribClass αᵒᵈ

Equations

⋯ = h

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

RightDistribClass αᵒᵈ

Equations

⋯ = 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 instHasDistribNegOrderDual {α : Type u_1} [Mul α] [h : HasDistribNeg α] :

HasDistribNeg αᵒᵈ

Equations

instHasDistribNegOrderDual = 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 α] :

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 instIsDomainOrderDual {α : Type u_1} [Ring α] [h : IsDomain α] :

IsDomain αᵒᵈ

Equations

⋯ = h

Lexicographical order #

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

Distrib (Lex α)

Equations

instDistribLex = h

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

LeftDistribClass (Lex α)

Equations

⋯ = h

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

RightDistribClass (Lex α)

Equations

⋯ = 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 instHasDistribNegLex {α : Type u_1} [Mul α] [h : HasDistribNeg α] :

HasDistribNeg (Lex α)

Equations

instHasDistribNegLex = 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 α] :

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 instIsDomainLex {α : Type u_1} [Ring α] [h : IsDomain α] :

IsDomain (Lex α)

Equations

⋯ = h