diff options
Diffstat (limited to 'src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda')
| -rw-r--r-- | src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda | 4 |
1 files changed, 3 insertions, 1 deletions
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 ) |