From b75264cfcc2e2b9a999205acda93353ded1b9cfe Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 5 Apr 2022 12:10:47 +0100 Subject: Add properties of multiplying to 0. --- src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda') diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda index c0207a3..bfd38b7 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda @@ -97,7 +97,7 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public ; x>1∧y≥1⇒x*y>1; x≥1∧y>1⇒x*y>1; 0≤x<1∧y≤1⇒x*y<1; x≤1∧0≤y<1⇒x*y<1 ; x≥1∧y≥1⇒x*y≥1; 0≤x≤1∧y≤1⇒x*y≤1; x≤1∧0≤y≤1⇒x*y≤1 - ; x*x≥0 + ; x*x≥0; x*y≈0⇒x≈0⊎y≈0 ; ^-zeroˡ; ^-zeroʳ ; ^-identityʳ @@ -109,6 +109,8 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public ; x>0⇒x^n>0 ; x≥0⇒x^n≥0 + ; x^n≈0⇒x≈0 + ; x>1∧n≢0⇒x^n>1; 0≤x<1∧n≢0⇒x^n<1 ; x≥1⇒x^n≥1; 0≤x≤1⇒x^n≤1 ) -- cgit v1.2.3