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 α] :
instance instSemiringOrderDual {α : Type u_1} [h : Semiring α] :
instance instRingOrderDual {α : Type u_1} [h : Ring α] :
instance instCommRingOrderDual {α : Type u_1} [h : CommRing α] :

Lexicographical order #

instance instDistribLex {α : Type u_1} [h : Distrib α] :
instance instSemiringLex {α : Type u_1} [h : Semiring α] :
instance instCommSemiringLex {α : Type u_1} [h : CommSemiring α] :
instance instNonAssocRingLex {α : Type u_1} [h : NonAssocRing α] :
instance instRingLex {α : Type u_1} [h : Ring α] :
Ring (Lex α)
instance instCommRingLex {α : Type u_1} [h : CommRing α] :