diff options
Diffstat (limited to 'src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda')
| -rw-r--r-- | src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda index db070e0..c83f683 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda @@ -105,11 +105,13 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.AbelianGroup +-abelian ; ⁻¹-anti-cancel-< to -‿anti-cancel-< ; ⁻¹-anti-cancel-≤ to -‿anti-cancel-≤ + ; x≈ε⇒x⁻¹≈ε to x≈0⇒-x≈0 ; x<ε⇒x⁻¹>ε to x<0⇒-x>0 ; x>ε⇒x⁻¹<ε to x>0⇒-x<0 ; x≤ε⇒x⁻¹≥ε to x≤0⇒-x≥0 ; x≥ε⇒x⁻¹≤ε to x≥0⇒-x≤0 + ; x⁻¹≈ε⇒x≈ε to -x≈0⇒x≈0 ; x⁻¹<ε⇒x>ε to -x<0⇒x>0 ; x⁻¹>ε⇒x<ε to -x>0⇒x<0 ; x⁻¹≤ε⇒x≥ε to -x≤0⇒x≥0 |