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