diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-04-05 12:10:47 +0100 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-04-05 12:10:47 +0100 |
| commit | b75264cfcc2e2b9a999205acda93353ded1b9cfe (patch) | |
| tree | 7c806556a9be5991457fdb8f23519e5ce4c59f35 /src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda | |
| parent | 038d2109e78d9c688acfc3338140cc908151db76 (diff) | |
Add properties of multiplying to 0.
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 ) |