Ordered ring instances for MulOpposite/AddOpposite

This files transfers ordered (semi)ring instances from α to αᵐᵒᵖ and αᵃᵒᵖ.

instance MulOpposite.instOrderedSemiring {α : Type u_1} [OrderedSemiring α] : OrderedSemiring αᵐᵒᵖ

Equations

• MulOpposite.instOrderedSemiring = OrderedSemiring.mk ⋯ ⋯ ⋯ ⋯

instance MulOpposite.instOrderedRing {α : Type u_1} [OrderedRing α] : OrderedRing αᵐᵒᵖ

Equations

• MulOpposite.instOrderedRing = OrderedRing.mk ⋯ ⋯ ⋯

instance AddOpposite.instOrderedSemiring {α : Type u_1} [OrderedSemiring α] : OrderedSemiring αᵃᵒᵖ

Equations

• AddOpposite.instOrderedSemiring = OrderedSemiring.mk ⋯ ⋯ ⋯ ⋯

instance AddOpposite.instOrderedRingMulOpposite {α : Type u_1} [OrderedRing α] : OrderedRing αᵐᵒᵖ

Equations

• AddOpposite.instOrderedRingMulOpposite = OrderedRing.mk ⋯ ⋯ ⋯