Products of ordered rings

instance instOrderedSemiringProd {α : Type u_1} {β : Type u_2} [OrderedSemiring α] [OrderedSemiring β] : OrderedSemiring (α × β)

Equations

• instOrderedSemiringProd = OrderedSemiring.mk ⋯ ⋯ ⋯ ⋯

instance instOrderedCommSemiringProd {α : Type u_1} {β : Type u_2} [OrderedCommSemiring α] [OrderedCommSemiring β] : OrderedCommSemiring (α × β)

Equations

• instOrderedCommSemiringProd = OrderedCommSemiring.mk ⋯

instance instOrderedRingProd {α : Type u_1} {β : Type u_2} [OrderedRing α] [OrderedRing β] : OrderedRing (α × β)

Equations

• instOrderedRingProd = OrderedRing.mk ⋯ ⋯ ⋯

instance instOrderedCommRingProd {α : Type u_1} {β : Type u_2} [OrderedCommRing α] [OrderedCommRing β] : OrderedCommRing (α × β)

Equations

• instOrderedCommRingProd = OrderedCommRing.mk ⋯