From 5202560ea008a76048587f6ab63797f7517fbdc0 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Mon, 21 Mar 2022 16:37:12 +0000
Subject: Add some properties of algebraic pseudocode types.

---
 .../StrictTotal/Properties/CommutativeRing.agda    | 27 ++++++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda

(limited to 'src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda')

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)
-- 
cgit v1.2.3