From ba95dc7d15cab1af40da896114b7dd9aad5afda0 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Sat, 2 Apr 2022 14:18:28 +0100
Subject: Add some properties of ordered fields.

---
 .../StrictTotal/Properties/DivisionRing.agda       | 100 +++++++++++++++++++++
 .../Ordered/StrictTotal/Properties/Field.agda      | 100 +++++++++++++++++++++
 2 files changed, 200 insertions(+)
 create mode 100644 src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
 create mode 100644 src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda

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

diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
new file mode 100644
index 0000000..f9f0376
--- /dev/null
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
@@ -0,0 +1,100 @@
+------------------------------------------------------------------------
+--  Agda Helium
+--
+-- Algebraic properties of ordered division rings
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Helium.Algebra.Ordered.StrictTotal.Bundles
+
+module Helium.Algebra.Ordered.StrictTotal.Properties.DivisionRing
+  {ℓ₁ ℓ₂ ℓ₃}
+  (divisionRing : DivisionRing ℓ₁ ℓ₂ ℓ₃)
+  where
+
+open DivisionRing divisionRing
+  renaming
+  ( trans to <-trans
+  ; irrefl to <-irrefl
+  ; asym to <-asym
+  ; 0<a+0<b⇒0<ab to x>0∧y>0⇒x*y>0
+  )
+
+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.Semiring.Exp.TCOptimised Unordered.semiring public
+open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public
+open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public
+  using
+  ( +-mono-<; +-monoˡ-<; +-monoʳ-<
+  ; +-mono-≤; +-monoˡ-≤; +-monoʳ-≤
+
+  ; +-cancel-<; +-cancelˡ-<; +-cancelʳ-<
+  ; +-cancel-≤; +-cancelˡ-≤; +-cancelʳ-≤
+
+  ; x≥0∧y>0⇒x+y>0 ; x>0∧y≥0⇒x+y>0
+  ; x≤0∧y<0⇒x+y<0 ; x<0∧y≤0⇒x+y<0
+  ; x≥0∧y≥0⇒x+y≥0 ; x≤0∧y≤0⇒x+y≤0
+
+  ; x≤0∧x+y>0⇒y>0 ; x≤0∧y+x>0⇒y>0 ; x<0∧x+y≥0⇒y>0 ; x<0∧y+x≥0⇒y>0
+  ; x≥0∧x+y<0⇒y<0 ; x≥0∧y+x<0⇒y<0 ; x>0∧x+y≤0⇒y<0 ; x>0∧y+x≤0⇒y<0
+  ; x≤0∧x+y≥0⇒y≥0 ; x≤0∧y+x≥0⇒y≥0
+  ; x≥0∧x+y≤0⇒y≤0 ; x≥0∧y+x≤0⇒y≤0
+
+  ; ×-zeroˡ; ×-zeroʳ
+  ; ×-identityˡ
+
+  ; n≢0⇒×-monoˡ-< ; x>0⇒×-monoʳ-< ; x<0⇒×-anti-monoʳ-<
+  ; ×-monoˡ-≤; x≥0⇒×-monoʳ-≤; x≤0⇒×-anti-monoʳ-≤
+
+  ; ×-cancelˡ-<; x≥0⇒×-cancelʳ-<; x≤0⇒×-anti-cancelʳ-<
+  ; n≢0⇒×-cancelˡ-≤ ; x>0⇒×-cancelʳ-≤ ; x<0⇒×-anti-cancelʳ-≤
+
+  ; n≢0∧x>0⇒n×x>0; n≢0∧x<0⇒n×x<0
+  ; x≥0⇒n×x≥0; x≤0⇒n×x≤0
+
+  ; n×x>0⇒x>0; n×x<0⇒x<0
+  ; n≢0∧n×x≥0⇒x≥0; n≢0∧n×x≤0⇒x≤0
+
+  ; -‿anti-mono-<; -‿anti-mono-≤
+  ; -‿cancel; -‿anti-cancel-<; -‿anti-cancel-≤
+
+  ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0
+  ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0
+
+  ; x<y⇒0<y-x; 0<y-x⇒x<y
+
+  ; 0≤1; 1≈0⇒x≈y; x<y⇒0<1
+
+  ; x>0⇒*-monoˡ-<; x>0⇒*-monoʳ-<; x<0⇒*-anti-monoˡ-<; x<0⇒*-anti-monoʳ-<
+  ; x≥0⇒*-monoˡ-≤; x≥0⇒*-monoʳ-≤; x≤0⇒*-anti-monoˡ-≤; x≤0⇒*-anti-monoʳ-≤
+
+  ; x≥0⇒*-cancelˡ-<; x≥0⇒*-cancelʳ-<; x≤0⇒*-anti-cancelˡ-<; x≤0⇒*-anti-cancelʳ-<
+  ; x>0⇒*-cancelˡ-≤; x>0⇒*-cancelʳ-≤; x<0⇒*-anti-cancelˡ-≤; x<0⇒*-anti-cancelʳ-≤
+
+  ; x≈0⇒x*y≈0; x≈0⇒y*x≈0
+
+  ; -x*-y≈x*y
+  ;                x>0∧y<0⇒x*y<0; x<0∧y>0⇒x*y<0; x<0∧y<0⇒x*y>0
+  ; x≥0∧y≥0⇒x*y≥0; x≥0∧y≤0⇒x*y≤0; x≤0∧y≥0⇒x*y≤0; x≤0∧y≤0⇒x*y≥0
+
+  ; x>1∧y≥1⇒x*y>1; x≥1∧y>1⇒x*y>1; 0≤x<1∧y≤1⇒x*y<1; x≤1∧0≤y<1⇒x*y<1
+  ; x≥1∧y≥1⇒x*y≥1; 0≤x≤1∧y≤1⇒x*y≤1; x≤1∧0≤y≤1⇒x*y≤1
+
+  ; x*x≥0
+
+  ; ^-zeroˡ; ^-zeroʳ
+  ; ^-identityʳ
+
+  ; n≢0⇒0^n≈0
+  ; x>1⇒^-monoˡ-<; 0<x<1⇒^-anti-monoˡ-<
+  ; x≥1⇒^-monoˡ-≤; 0≤x≤1⇒^-anti-monoˡ-≤
+
+  ; x>0⇒x^n>0
+  ; x≥0⇒x^n≥0
+
+  ; x>1∧n≢0⇒x^n>1; 0≤x<1∧n≢0⇒x^n<1
+  ; x≥1⇒x^n≥1; 0≤x≤1⇒x^n≤1
+  )
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
new file mode 100644
index 0000000..1914a31
--- /dev/null
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
@@ -0,0 +1,100 @@
+------------------------------------------------------------------------
+--  Agda Helium
+--
+-- Algebraic properties of ordered fields
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Helium.Algebra.Ordered.StrictTotal.Bundles
+
+module Helium.Algebra.Ordered.StrictTotal.Properties.Field
+  {ℓ₁ ℓ₂ ℓ₃}
+  (field′ : Field ℓ₁ ℓ₂ ℓ₃)
+  where
+
+open Field field′
+  renaming
+  ( trans to <-trans
+  ; irrefl to <-irrefl
+  ; asym to <-asym
+  ; 0<a+0<b⇒0<ab to x>0∧y>0⇒x*y>0
+  )
+
+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.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public
+open import Helium.Algebra.Ordered.StrictTotal.Properties.DivisionRing divisionRing public
+  using
+  ( +-mono-<; +-monoˡ-<; +-monoʳ-<
+  ; +-mono-≤; +-monoˡ-≤; +-monoʳ-≤
+
+  ; +-cancel-<; +-cancelˡ-<; +-cancelʳ-<
+  ; +-cancel-≤; +-cancelˡ-≤; +-cancelʳ-≤
+
+  ; x≥0∧y>0⇒x+y>0 ; x>0∧y≥0⇒x+y>0
+  ; x≤0∧y<0⇒x+y<0 ; x<0∧y≤0⇒x+y<0
+  ; x≥0∧y≥0⇒x+y≥0 ; x≤0∧y≤0⇒x+y≤0
+
+  ; x≤0∧x+y>0⇒y>0 ; x≤0∧y+x>0⇒y>0 ; x<0∧x+y≥0⇒y>0 ; x<0∧y+x≥0⇒y>0
+  ; x≥0∧x+y<0⇒y<0 ; x≥0∧y+x<0⇒y<0 ; x>0∧x+y≤0⇒y<0 ; x>0∧y+x≤0⇒y<0
+  ; x≤0∧x+y≥0⇒y≥0 ; x≤0∧y+x≥0⇒y≥0
+  ; x≥0∧x+y≤0⇒y≤0 ; x≥0∧y+x≤0⇒y≤0
+
+  ; ×-zeroˡ; ×-zeroʳ
+  ; ×-identityˡ
+
+  ; n≢0⇒×-monoˡ-< ; x>0⇒×-monoʳ-< ; x<0⇒×-anti-monoʳ-<
+  ; ×-monoˡ-≤; x≥0⇒×-monoʳ-≤; x≤0⇒×-anti-monoʳ-≤
+
+  ; ×-cancelˡ-<; x≥0⇒×-cancelʳ-<; x≤0⇒×-anti-cancelʳ-<
+  ; n≢0⇒×-cancelˡ-≤ ; x>0⇒×-cancelʳ-≤ ; x<0⇒×-anti-cancelʳ-≤
+
+  ; n≢0∧x>0⇒n×x>0; n≢0∧x<0⇒n×x<0
+  ; x≥0⇒n×x≥0; x≤0⇒n×x≤0
+
+  ; n×x>0⇒x>0; n×x<0⇒x<0
+  ; n≢0∧n×x≥0⇒x≥0; n≢0∧n×x≤0⇒x≤0
+
+  ; -‿anti-mono-<; -‿anti-mono-≤
+  ; -‿cancel; -‿anti-cancel-<; -‿anti-cancel-≤
+
+  ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0
+  ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0
+
+  ; x<y⇒0<y-x; 0<y-x⇒x<y
+
+  ; 0≤1; 1≈0⇒x≈y; x<y⇒0<1
+
+  ; x>0⇒*-monoˡ-<; x>0⇒*-monoʳ-<; x<0⇒*-anti-monoˡ-<; x<0⇒*-anti-monoʳ-<
+  ; x≥0⇒*-monoˡ-≤; x≥0⇒*-monoʳ-≤; x≤0⇒*-anti-monoˡ-≤; x≤0⇒*-anti-monoʳ-≤
+
+  ; x≥0⇒*-cancelˡ-<; x≥0⇒*-cancelʳ-<; x≤0⇒*-anti-cancelˡ-<; x≤0⇒*-anti-cancelʳ-<
+  ; x>0⇒*-cancelˡ-≤; x>0⇒*-cancelʳ-≤; x<0⇒*-anti-cancelˡ-≤; x<0⇒*-anti-cancelʳ-≤
+
+  ; x≈0⇒x*y≈0; x≈0⇒y*x≈0
+
+  ; -x*-y≈x*y
+  ;                x>0∧y<0⇒x*y<0; x<0∧y>0⇒x*y<0; x<0∧y<0⇒x*y>0
+  ; x≥0∧y≥0⇒x*y≥0; x≥0∧y≤0⇒x*y≤0; x≤0∧y≥0⇒x*y≤0; x≤0∧y≤0⇒x*y≥0
+
+  ; x>1∧y≥1⇒x*y>1; x≥1∧y>1⇒x*y>1; 0≤x<1∧y≤1⇒x*y<1; x≤1∧0≤y<1⇒x*y<1
+  ; x≥1∧y≥1⇒x*y≥1; 0≤x≤1∧y≤1⇒x*y≤1; x≤1∧0≤y≤1⇒x*y≤1
+
+  ; x*x≥0
+
+  ; ^-zeroˡ; ^-zeroʳ
+  ; ^-identityʳ
+
+  ; n≢0⇒0^n≈0
+  ; x>1⇒^-monoˡ-<; 0<x<1⇒^-anti-monoˡ-<
+  ; x≥1⇒^-monoˡ-≤; 0≤x≤1⇒^-anti-monoˡ-≤
+
+  ; x>0⇒x^n>0
+  ; x≥0⇒x^n≥0
+
+  ; x>1∧n≢0⇒x^n>1; 0≤x<1∧n≢0⇒x^n<1
+  ; x≥1⇒x^n≥1; 0≤x≤1⇒x^n≤1
+  )
-- 
cgit v1.2.3