diff options
Diffstat (limited to 'src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda')
| -rw-r--r-- | src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda index 79d3b2d..eb46e27 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda @@ -126,7 +126,7 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.DivisionRing divisionR ; -‿⁻¹-comm ; x≉0⇒x⁻¹≉0 - ; y>0∧x<y⇒x*y⁻¹<1 + ; y>0∧x<y⇒x*y⁻¹<1; y>0∧x≤y⇒x*y⁻¹≤1 ) -------------------------------------------------------------------------------- |