diff options
Diffstat (limited to 'src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda')
| -rw-r--r-- | src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda index cad9714..aa37d59 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda @@ -63,9 +63,11 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Group group public ; ⁻¹-anti-cancel-<; ⁻¹-anti-cancel-≤ + ; x≈ε⇒x⁻¹≈ε ; x<ε⇒x⁻¹>ε; x>ε⇒x⁻¹<ε ; x≤ε⇒x⁻¹≥ε; x≥ε⇒x⁻¹≤ε + ; x⁻¹≈ε⇒x≈ε ; x⁻¹<ε⇒x>ε; x⁻¹>ε⇒x<ε ; x⁻¹≤ε⇒x≥ε; x⁻¹≥ε⇒x≤ε |