diff options
Diffstat (limited to 'src')
6 files changed, 4 insertions, 16 deletions
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda index a6cbcab..cad9714 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda @@ -61,7 +61,7 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Group group public ; ⁻¹-anti-mono-<; ⁻¹-anti-mono-≤ - ; ⁻¹-cancel; ⁻¹-anti-cancel-<; ⁻¹-anti-cancel-≤ + ; ⁻¹-anti-cancel-<; ⁻¹-anti-cancel-≤ ; x<ε⇒x⁻¹>ε; x>ε⇒x⁻¹<ε ; x≤ε⇒x⁻¹≥ε; x≥ε⇒x⁻¹≤ε diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda index d303c99..aa265c8 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda @@ -59,7 +59,7 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public ; n≢0∧n×x≥0⇒x≥0; n≢0∧n×x≤0⇒x≤0 ; -‿anti-mono-<; -‿anti-mono-≤ - ; -‿cancel; -‿anti-cancel-<; -‿anti-cancel-≤ + ; -‿anti-cancel-<; -‿anti-cancel-≤ ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0 ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0 diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda index f9f0376..4531605 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda @@ -59,7 +59,7 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public ; n≢0∧n×x≥0⇒x≥0; n≢0∧n×x≤0⇒x≤0 ; -‿anti-mono-<; -‿anti-mono-≤ - ; -‿cancel; -‿anti-cancel-<; -‿anti-cancel-≤ + ; -‿anti-cancel-<; -‿anti-cancel-≤ ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0 ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0 diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda index 1914a31..337947a 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda @@ -59,7 +59,7 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.DivisionRing divisionR ; n≢0∧n×x≥0⇒x≥0; n≢0∧n×x≤0⇒x≤0 ; -‿anti-mono-<; -‿anti-mono-≤ - ; -‿cancel; -‿anti-cancel-<; -‿anti-cancel-≤ + ; -‿anti-cancel-<; -‿anti-cancel-≤ ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0 ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0 diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda index d72ae10..cf8e4f2 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda @@ -94,17 +94,6 @@ open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder ---- Cancellative --- _≈_ - -⁻¹-cancel : Injective _≈_ _≈_ _⁻¹ -⁻¹-cancel {x} {y} x⁻¹≈y⁻¹ = begin-equality - x ≈⟨ inverseˡ-unique x (y ⁻¹) (begin-equality - x ∙ y ⁻¹ ≈˘⟨ ∙-congˡ x⁻¹≈y⁻¹ ⟩ - x ∙ x ⁻¹ ≈⟨ inverseʳ x ⟩ - ε ∎) ⟩ - y ⁻¹ ⁻¹ ≈⟨ ⁻¹-involutive y ⟩ - y ∎ - -- _<_ ⁻¹-anti-cancel-< : Injective _<_ _>_ _⁻¹ diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda index 5e51e89..eff2d37 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda @@ -102,7 +102,6 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.AbelianGroup +-abelian ; ⁻¹-anti-mono-< to -‿anti-mono-< ; ⁻¹-anti-mono-≤ to -‿anti-mono-≤ - ; ⁻¹-cancel to -‿cancel ; ⁻¹-anti-cancel-< to -‿anti-cancel-< ; ⁻¹-anti-cancel-≤ to -‿anti-cancel-≤ |