From ba95dc7d15cab1af40da896114b7dd9aad5afda0 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sat, 2 Apr 2022 14:18:28 +0100 Subject: Add some properties of ordered fields. --- src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda') diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda index 0f8df22..648d164 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda @@ -567,7 +567,7 @@ record Field c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where ( +-rawMagma; +-rawMonoid ; +-magma; +-semigroup; +-monoid; +-commutativeMonoid; +-group; +-abelianGroup ; rawSemiring; rawRing - ; semiring; ring; divisionRing + ; semiring; commutativeSemiring; ring; commutativeRing; divisionRing ) open IsField.Unordered isField public -- cgit v1.2.3