added CommutativeRing to the tally

Author: jamesmckinna

CHANGELOG.md

@@ -1602,7 +1602,9 @@ Other minor changes
   zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙)
   distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) +
   isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1#
+  isCommutativeRing : IsCommutativeRing ≈ + * - 0# 1# → IsCommutativeRing ≈ + (flip *) - 0# 1#
   ring : Ring a ℓ → Ring a ℓ
+  commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ
   ```
 
 * Added new definition to `Algebra.Definitions`:

src/Algebra/Construct/Flip/Op.agda

@@ -200,6 +200,14 @@ module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where
     where
       module r = IsRing r
 
+  isCommutativeRing : IsCommutativeRing + * - 0# 1# → IsCommutativeRing + (flip *) - 0# 1#
+  isCommutativeRing r = record
+    { isRing = isRing r.isRing
+    ; *-comm = commutative r.*-comm
+    }
+    where
+      module r = IsCommutativeRing r
+
 
 ------------------------------------------------------------------------
 -- Bundles
@@ -282,3 +290,7 @@ ring : Ring a ℓ → Ring a ℓ
 ring r = record { isRing = isRing r.isRing }
   where module r = Ring r
 
+commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ
+commutativeRing r = record { isCommutativeRing = isCommutativeRing r.isCommutativeRing }
+  where module r = CommutativeRing r
+