1 files changed, 27 insertions, 0 deletions
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda
new file mode 100644
index 0000000..24b2663
--- /dev/null
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda
@@ -0,0 +1,27 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Algebraic properties of ordered commutative rings
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Algebra.Ordered.StrictTotal.Bundles
+
+module Helium.Algebra.Ordered.StrictTotal.Properties.CommutativeRing
+  {ℓ₁ ℓ₂ ℓ₃}
+  (commutativeRing : CommutativeRing ℓ₁ ℓ₂ ℓ₃)
+  where
+
+open CommutativeRing commutativeRing
+
+open import Algebra.Properties.Ring Unordered.ring public
+  renaming (-0#≈0# to -0≈0)
+open import Algebra.Properties.Semiring.Mult.TCOptimised Unordered.semiring public
+open import Algebra.Properties.CommutativeSemiring.Exp.TCOptimised Unordered.commutativeSemiring public
+open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public
+  using
+  ( <⇒≱; ≤⇒≯; >⇒≉; ≈⇒≯; <⇒≉; ≈⇒≮; ≤∧≉⇒<; ≥∧≉⇒>
+  ; x<y⇒0<y-x; -‿anti-mono
+  ; ⊤′; number; negative
+  ; 0≤1; 1≉0+n≉0⇒0<+n; 1≉0+n≉0⇒-n<0)