feat: port algebra.ring.order_synonym (#671)

mathlib3 sha: 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

Mathlib.lean

@@ -24,6 +24,7 @@ import Mathlib.Algebra.PEmptyInstances
 import Mathlib.Algebra.Quotient
 import Mathlib.Algebra.Ring.Basic
 import Mathlib.Algebra.Ring.Defs
+import Mathlib.Algebra.Ring.OrderSynonym
 import Mathlib.CategoryTheory.ConcreteCategory.Bundled
 import Mathlib.Control.EquivFunctor
 import Mathlib.Control.Random

Mathlib/Algebra/Ring/OrderSynonym.lean

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2021 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov, Yaël Dillies
+-/
+import Mathlib.Algebra.Ring.Defs
+import Mathlib.Algebra.Group.OrderSynonym
+
+/-!
+# Ring structure on the order type synonyms
+
+Transfer algebraic instances from `α` to `αᵒᵈ` and `lex α`.
+-/
+
+
+variable {α : Type _}
+
+/-! ### Order dual -/
+
+
+instance [h : Distrib α] : Distrib αᵒᵈ := h
+
+instance [Mul α] [Add α] [h : LeftDistribClass α] : LeftDistribClass αᵒᵈ := h
+
+instance [Mul α] [Add α] [h : RightDistribClass α] : RightDistribClass αᵒᵈ := h
+
+instance [h : NonUnitalNonAssocSemiring α] : NonUnitalNonAssocSemiring αᵒᵈ := h
+
+instance [h : NonUnitalSemiring α] : NonUnitalSemiring αᵒᵈ := h
+
+instance [h : NonAssocSemiring α] : NonAssocSemiring αᵒᵈ := h
+
+instance [h : Semiring α] : Semiring αᵒᵈ := h
+
+instance [h : NonUnitalCommSemiring α] : NonUnitalCommSemiring αᵒᵈ := h
+
+instance [h : CommSemiring α] : CommSemiring αᵒᵈ := h
+
+instance [Mul α] [h : HasDistribNeg α] : HasDistribNeg αᵒᵈ := h
+
+instance [h : NonUnitalNonAssocRing α] : NonUnitalNonAssocRing αᵒᵈ := h
+
+instance [h : NonUnitalRing α] : NonUnitalRing αᵒᵈ := h
+
+instance [h : NonAssocRing α] : NonAssocRing αᵒᵈ := h
+
+instance [h : Ring α] : Ring αᵒᵈ := h
+
+instance [h : NonUnitalCommRing α] : NonUnitalCommRing αᵒᵈ := h
+
+instance [h : CommRing α] : CommRing αᵒᵈ := h
+
+instance [Ring α] [h : IsDomain α] : IsDomain αᵒᵈ := h
+
+/-! ### Lexicographical order -/
+
+
+instance [h : Distrib α] : Distrib (Lex α) := h
+
+instance [Mul α] [Add α] [h : LeftDistribClass α] : LeftDistribClass (Lex α) := h
+
+instance [Mul α] [Add α] [h : RightDistribClass α] : RightDistribClass (Lex α) := h
+
+instance [h : NonUnitalNonAssocSemiring α] : NonUnitalNonAssocSemiring (Lex α) := h
+
+instance [h : NonUnitalSemiring α] : NonUnitalSemiring (Lex α) := h
+
+instance [h : NonAssocSemiring α] : NonAssocSemiring (Lex α) := h
+
+instance [h : Semiring α] : Semiring (Lex α) := h
+
+instance [h : NonUnitalCommSemiring α] : NonUnitalCommSemiring (Lex α) := h
+
+instance [h : CommSemiring α] : CommSemiring (Lex α) := h
+
+instance [Mul α] [h : HasDistribNeg α] : HasDistribNeg (Lex α) := h
+
+instance [h : NonUnitalNonAssocRing α] : NonUnitalNonAssocRing (Lex α) := h
+
+instance [h : NonUnitalRing α] : NonUnitalRing (Lex α) := h
+
+instance [h : NonAssocRing α] : NonAssocRing (Lex α) := h
+
+instance [h : Ring α] : Ring (Lex α) := h
+
+instance [h : NonUnitalCommRing α] : NonUnitalCommRing (Lex α) := h
+
+instance [h : CommRing α] : CommRing (Lex α) := h
+
+instance [Ring α] [h : IsDomain α] : IsDomain (Lex α) := h