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 α] :
Equations
  • instDistribOrderDual = h
Equations
  • instNonUnitalNonAssocSemiringOrderDual = h
Equations
  • instNonUnitalSemiringOrderDual = h
Equations
  • instNonAssocSemiringOrderDual = h
instance instSemiringOrderDual {α : Type u_1} [h : Semiring α] :
Equations
  • instSemiringOrderDual = h
Equations
  • instNonUnitalCommSemiringOrderDual = h
Equations
  • instCommSemiringOrderDual = h
Equations
  • instHasDistribNegOrderDualInstMulOrderDual = h
Equations
  • instNonUnitalNonAssocRingOrderDual = h
Equations
  • instNonUnitalRingOrderDual = h
Equations
  • instNonAssocRingOrderDual = h
instance instRingOrderDual {α : Type u_1} [h : Ring α] :
Equations
  • instRingOrderDual = h
Equations
  • instNonUnitalCommRingOrderDual = h
instance instCommRingOrderDual {α : Type u_1} [h : CommRing α] :
Equations
  • instCommRingOrderDual = h

Lexicographical order #

instance instDistribLex {α : Type u_1} [h : Distrib α] :
Equations
  • instDistribLex = h
Equations
  • instNonUnitalNonAssocSemiringLex = h
Equations
  • instNonUnitalSemiringLex = h
Equations
  • instNonAssocSemiringLex = h
instance instSemiringLex {α : Type u_1} [h : Semiring α] :
Equations
  • instSemiringLex = h
Equations
  • instNonUnitalCommSemiringLex = h
instance instCommSemiringLex {α : Type u_1} [h : CommSemiring α] :
Equations
  • instCommSemiringLex = h
instance instHasDistribNegLexInstMulLex {α : Type u_1} [Mul α] [h : HasDistribNeg α] :
Equations
  • instHasDistribNegLexInstMulLex = h
Equations
  • instNonUnitalNonAssocRingLex = h
instance instNonUnitalRingLex {α : Type u_1} [h : NonUnitalRing α] :
Equations
  • instNonUnitalRingLex = h
instance instNonAssocRingLex {α : Type u_1} [h : NonAssocRing α] :
Equations
  • instNonAssocRingLex = h
instance instRingLex {α : Type u_1} [h : Ring α] :
Ring (Lex α)
Equations
  • instRingLex = h
Equations
  • instNonUnitalCommRingLex = h
instance instCommRingLex {α : Type u_1} [h : CommRing α] :
Equations
  • instCommRingLex = h
instance instIsDomainLexInstSemiringLexToSemiring {α : Type u_1} [Ring α] [h : IsDomain α] :
Equations