opposite of a Ring

CHANGELOG.md

@@ -1587,6 +1587,14 @@ Other minor changes
   moufangLoop : MoufangLoop a ℓ₁ → MoufangLoop b ℓ₂ → MoufangLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
  ```
 
+* Added new functions and proofs to `Algebra.Construct.Flip.Op`:
+  ```agda
+  zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙)
+  distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) +
+  isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1#
+  ring : Ring a ℓ → Ring a ℓ
+  ```
+
 * Added new definition to `Algebra.Definitions`:
   ```agda
   LeftDividesˡ  : Op₂ A → Op₂ A → Set _

src/Algebra/Construct/Flip/Op.agda

@@ -53,6 +53,14 @@ module _ (≈ : Rel A ℓ) (∙ : Op₂ A) where
   inverse : Inverse ≈ ε ⁻¹ ∙ → Inverse ≈ ε ⁻¹ (flip ∙)
   inverse inv = Prod.swap inv
 
+  zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙)
+  zero zer = Prod.swap zer
+
+  module _ (+ : Op₂ A) where
+
+    distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) +
+    distributes distrib = Prod.swap distrib
+
 ------------------------------------------------------------------------
 -- Structures
 
@@ -163,6 +171,23 @@ module _ {≈ : Rel A ℓ} {∙ : Op₂ A} where
     }
     where module g = IsAbelianGroup g
 
+module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where
+
+  isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1#
+  isRing r = record
+    { +-isAbelianGroup = r-isAbelianGroup
+    ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong
+    ; *-assoc = associative ≈ * sym r.*-assoc
+    ; *-identity = identity ≈ * r.*-identity
+    ; distrib = distributes ≈ * + r.distrib
+    ; zero = zero ≈ * r.zero
+    }
+    where
+      module r = IsRing r
+      r-isAbelianGroup = r.+-isAbelianGroup
+      open IsAbelianGroup r-isAbelianGroup using (sym)
+
+
 ------------------------------------------------------------------------
 -- Bundles
 
@@ -239,3 +264,7 @@ group g = record { isGroup = isGroup g.isGroup }
 abelianGroup : AbelianGroup a ℓ → AbelianGroup a ℓ
 abelianGroup g = record { isAbelianGroup = isAbelianGroup g.isAbelianGroup }
   where module g = AbelianGroup g
+
+ring : Ring a ℓ → Ring a ℓ
+ring r = record { isRing = isRing r.isRing }
+  where module r = Ring r