diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-04-09 16:24:18 +0100 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-04-09 16:24:18 +0100 |
| commit | c6aee22d68aa614619cecc08a15332294a9de0de (patch) | |
| tree | 6b589e18b902c21d481bedf278f51123a5f55ac9 /src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda | |
| parent | 662ca19ed7dabecdf17cdd555132f106bb768e58 (diff) | |
Add some more algebraic properties.
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 ) -------------------------------------------------------------------------------- |