Add properties of multiplying to 0.

4 files changed, 30 insertions, 4 deletions

diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda
index 6eba0ab..95e43ba 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda
@@ -84,7 +84,7 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public
   ; 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
+  ; x*x≥0; x*y≈0⇒x≈0⊎y≈0
 
   ; ^-zeroˡ; ^-zeroʳ
   ; ^-identityʳ
@@ -96,6 +96,8 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public
   ; x>0⇒x^n>0
   ; x≥0⇒x^n≥0
 
+  ; x^n≈0⇒x≈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/DivisionRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
index c0207a3..bfd38b7 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
@@ -97,7 +97,7 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public
   ; 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
+  ; x*x≥0; x*y≈0⇒x≈0⊎y≈0
 
   ; ^-zeroˡ; ^-zeroʳ
   ; ^-identityʳ
@@ -109,6 +109,8 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public
   ; x>0⇒x^n>0
   ; x≥0⇒x^n≥0
 
+  ; x^n≈0⇒x≈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
index f3ab1c1..45d0cfa 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
@@ -94,7 +94,7 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.DivisionRing divisionR
   ; 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
+  ; x*x≥0; x*y≈0⇒x≈0⊎y≈0
 
   ; ^-zeroˡ; ^-zeroʳ
   ; ^-identityʳ
@@ -106,6 +106,8 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.DivisionRing divisionR
   ; x>0⇒x^n>0
   ; x≥0⇒x^n≥0
 
+  ; x^n≈0⇒x≈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/Ring.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda
index 5c35176..624cd21 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda
@@ -22,8 +22,9 @@ open Ring ring
   )
 
 open import Algebra.Definitions
+open import Data.Empty using (⊥-elim)
 open import Data.Nat as ℕ using (suc; NonZero)
-open import Data.Sum using (inj₁; inj₂)
+open import Data.Sum using (_⊎_; inj₁; inj₂; fromInj₂)
 open import Function using (_∘_)
 open import Function.Definitions
 open import Helium.Algebra.Ordered.StrictTotal.Consequences strictTotalOrder
@@ -441,6 +442,18 @@ x*x≥0 x with compare x 0#
 ... | tri≈ _ x≈0 _ = ≤-reflexive (Eq.sym (x≈0⇒x*y≈0 x≈0 x))
 ... | tri> _ _ x>0 = <⇒≤ (x>0∧y>0⇒x*y>0 x>0 x>0)
 
+x*y≈0⇒x≈0⊎y≈0 : ∀ {x y} → x * y ≈ 0# → x ≈ 0# ⊎ y ≈ 0#
+x*y≈0⇒x≈0⊎y≈0 {x} {y} x*y≈0 with compare x 0#
+x*y≈0⇒x≈0⊎y≈0 {x} {y} x*y≈0 | tri< x<0 _ _ with compare y 0#
+... | tri< y<0 _ _ = ⊥-elim (<-irrefl (Eq.sym x*y≈0) (x<0∧y<0⇒x*y>0 x<0 y<0))
+... | tri≈ _ y≈0 _ = inj₂ y≈0
+... | tri> _ _ y>0 = ⊥-elim (<-irrefl x*y≈0 (x<0∧y>0⇒x*y<0 x<0 y>0))
+x*y≈0⇒x≈0⊎y≈0 {x} {y} x*y≈0 | tri≈ _ x≈0 _ = inj₁ x≈0
+x*y≈0⇒x≈0⊎y≈0 {x} {y} x*y≈0 | tri> _ _ x>0 with compare y 0#
+... | tri< y<0 _ _ = ⊥-elim (<-irrefl x*y≈0 (x>0∧y<0⇒x*y<0 x>0 y<0))
+... | tri≈ _ y≈0 _ = inj₂ y≈0
+... | tri> _ _ y>0 = ⊥-elim (<-irrefl (Eq.sym x*y≈0) (x>0∧y>0⇒x*y>0 x>0 y>0))
+
 --------------------------------------------------------------------------------
 ---- Properties of _^_
 
@@ -482,6 +495,13 @@ x>0⇒x^n>0 {x} x>0 (suc n) = begin-strict
   x * x ^ n ≈˘⟨ ^-homo-* x 1 n ⟩
   x ^ suc n ∎
 
+---- Respects sign
+
+x^n≈0⇒x≈0 : ∀ x n → x ^ n ≈ 0# → x ≈ 0#
+x^n≈0⇒x≈0 x 0             x^n≈0 = 1≈0⇒x≈y x^n≈0
+x^n≈0⇒x≈0 x 1             x^n≈0 = x^n≈0
+x^n≈0⇒x≈0 x (suc (suc n)) x^n≈0 = fromInj₂ (x^n≈0⇒x≈0 x (suc n)) (x*y≈0⇒x≈0⊎y≈0 x^n≈0)
+
 ---- Preserves size
 
 -- _≤_