Products of star-ordered rings #
instance
Prod.instStarOrderedRing
{α : Type u_1}
{β : Type u_2}
[NonUnitalSemiring α]
[NonUnitalSemiring β]
[PartialOrder α]
[PartialOrder β]
[StarRing α]
[StarRing β]
[StarOrderedRing α]
[StarOrderedRing β]
:
StarOrderedRing (α × β)
Equations
- ⋯ = ⋯