Products of ordered rings #
instance
instOrderedSemiringProd
{α : Type u_1}
{β : Type u_2}
[OrderedSemiring α]
[OrderedSemiring β]
:
OrderedSemiring (α × β)
Equations
- instOrderedSemiringProd = let __src := inferInstanceAs (Semiring (α × β)); let __src_1 := inferInstanceAs (OrderedAddCommMonoid (α × β)); OrderedSemiring.mk ⋯ ⋯ ⋯ ⋯
instance
instOrderedCommSemiringProd
{α : Type u_1}
{β : Type u_2}
[OrderedCommSemiring α]
[OrderedCommSemiring β]
:
OrderedCommSemiring (α × β)
Equations
- instOrderedCommSemiringProd = let __src := inferInstanceAs (OrderedSemiring (α × β)); let __src_1 := inferInstanceAs (CommSemiring (α × β)); OrderedCommSemiring.mk ⋯
instance
instOrderedRingProd
{α : Type u_1}
{β : Type u_2}
[OrderedRing α]
[OrderedRing β]
:
OrderedRing (α × β)
Equations
- instOrderedRingProd = let __src := inferInstanceAs (Ring (α × β)); let __src_1 := inferInstanceAs (OrderedAddCommGroup (α × β)); OrderedRing.mk ⋯ ⋯ ⋯
instance
instOrderedCommRingProd
{α : Type u_1}
{β : Type u_2}
[OrderedCommRing α]
[OrderedCommRing β]
:
OrderedCommRing (α × β)
Equations
- instOrderedCommRingProd = let __src := inferInstanceAs (OrderedRing (α × β)); let __src_1 := inferInstanceAs (CommRing (α × β)); OrderedCommRing.mk ⋯