Ordered ring instances for MulOpposite/AddOpposite #
This files transfers ordered (semi)ring instances from R to Rᵐᵒᵖ and Rᵃᵒᵖ.
instance
MulOpposite.instIsOrderedRing
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
:
instance
AddOpposite.instIsOrderedRing
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
: